GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&cc=~nfrisby&order=priority
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&cc=~nfrisby&order=priority
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/2255
http://ghc.haskell.org/trac/ghc/ticket/2255#2255: Improve SpecConstr for free variablesThu, 01 May 2008 07:43:45 GMTsimonpj<p>
This ticket records a suggestion for improving <tt>SpecConstr</tt>, so we don't lose it. The original <tt>SpecConstr</tt> transformation is described in "<a class="ext-link" href="http://research.microsoft.com/%7Esimonpj/papers/spec-constr"><span class="icon"></span>Call pattern specialisation for Haskell</a>". Consider this program
</p>
<pre class="wiki"> f x = let g y = ...case x of { z:zs -> e1; [] -> e2 } ...
in
...case x of
z:zs -> if ... then g 3 else g 4
[] -> ...
</pre><p>
Here 'x' is free in 'g', but x's value is known at g's call sites. It's not enough just to know "x is a cons" inside g; we must also have access to z,zs. So perhaps the thing to do is to imagine lambda-lifting 'g' to become 'gl' thus:
</p>
<pre class="wiki"> gl x y = ...case x of { z:zs -> e1; [] -> e2 } ...
f x = ...case x of
z:zs -> if ... then gl x 3 else gl x 4
[] -> ...
</pre><p>
Now the <tt>SpecConstr</tt> transformation will apply nicely. And it's arguably a bad shortcoming that currently the mere act of lambda lifting can affect how effective <tt>SpecConstr</tt> is.
</p>
<p>
Of course, we only want to lambda-lift wrt the parameters that'll be specialised, so this transformation probably wants to be done at the same time as the rest of <tt>SpecConstr</tt>. I don't have much idea of how hard that'd be, but it's a nice idea.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2255#changelog
http://ghc.haskell.org/trac/ghc/ticket/5075
http://ghc.haskell.org/trac/ghc/ticket/5075#5075: CPR optimisation for sum types if only one constructor is usedFri, 01 Apr 2011 21:03:24 GMTbatterseapower<p>
Inspired by <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3138" title="bug: Returning a known constructor: GHC generates terrible code for cmonad (new)">#3138</a>, it might be useful for StrAnal to detect functions such as the following where only one of the data constructors for a sum type are CPRed:
</p>
<pre class="wiki">loop x = case x < 10 of True -> Left x; False -> loop (x*2)
</pre><p>
We can usefully transform to:
</p>
<pre class="wiki">$wloop x = case (case x < 10 of True -> Left x; False -> loop (x*2)) of Left y -> (# y #)
loop x = case loop x of (# y #) -> Left y
</pre><p>
Attached patch implements this behaviour. Most of the complication in the new code occurs because adding a DataCon field to the Demand data type means that we have to define a separate IfaceDemand type for storage in interface files.
</p>
<p>
The patch validates but I haven't done any tests on nofib. I have confirmed that the new optimisation hits on some examples, though.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/5075#changelog
http://ghc.haskell.org/trac/ghc/ticket/6018
http://ghc.haskell.org/trac/ghc/ticket/6018#6018: Injective type familiesWed, 18 Apr 2012 16:22:24 GMTlunaris<p>
Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
</p>
<p>
I've naively attempted a proof-of-concept in GHC. It's almost certainly incorrect and probably breaks the type system, but I thought it best to put it here and see if it can be made workable.
</p>
<p>
In summary, my changes are:
</p>
<ul><li>Add a new keyword, <tt>injective</tt>, which is available only when the <tt>TypeFamilies</tt> extension is enabled. Injective families may then be defined thus:
</li></ul><pre class="wiki"> injective family F a :: *
type instance F Int = Bool
type instance F Bool = Int
injective family G a :: *
type instance G a = a
</pre><blockquote>
<p>
Syntax is of course completely changeable; I've simply picked one of the possible designs. Hopefully this won't be subjected to too much bike-shedding.
</p>
</blockquote>
<ul><li>Add the constructor <tt>InjFamilyTyCon</tt> to <tt>TyConRhs</tt> and the family flavour <tt>InjectiveFamily</tt> to <tt>HsSyn</tt>. Again, I've opted to encode injectivity as a flavour rather than (say) a <tt>Bool</tt> attached to type families. This is a completely arbitrary choice and may be utterly stupid.
</li></ul><ul><li>Altered the definition of decomposable <tt>TyCon</tt>s to include injective families (<tt>isDecomposableTyCon</tt>). This effectively introduces a typing rule that says if we have <tt>(F a ~ F b)</tt> then we can deduce <tt>(a ~ b)</tt> (<tt>TcCanonical</tt>).
</li></ul><ul><li>Modified the unifier so that it will attempt to replace saturated injective families with their left-hand sides where possible (<tt>TcUnify</tt>). This means that in a function such as:
</li></ul><pre class="wiki"> f :: F a -> F a
f = ...
</pre><blockquote>
<p>
The type of <tt>f False</tt> is inferred as <tt>F Int</tt> (i.e., <tt>a</tt> is no longer ambiguous).
</p>
</blockquote>
<p>
Some things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate <tt>f False</tt> I get nothing (not even a Segmentation fault).
</p>
<p>
See what you think.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/6018#changelog
http://ghc.haskell.org/trac/ghc/ticket/7109
http://ghc.haskell.org/trac/ghc/ticket/7109#7109: Inlining depends on datatype size, even with INLINE pragmasWed, 01 Aug 2012 13:11:45 GMTdreixel<p>
Consider the following code:
</p>
<pre class="wiki">data Logic = T | F
| Not Logic
instance GEq Logic
testEqLogic = geq (Not T) (Not F)
</pre><p>
With a proper definitions of generic equality <tt>geq</tt> in class <tt>GEq</tt>, and an <tt>instance Generic Logic</tt>, we get the following core code with -O1:
</p>
<pre class="wiki">Rec {
Bug.$fGEqLogic_$cgeq [Occ=LoopBreaker]
:: Bug.Logic -> Bug.Logic -> GHC.Types.Bool
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType SS]
Bug.$fGEqLogic_$cgeq =
\ (x_ap1 :: Bug.Logic) (y_ap2 :: Bug.Logic) ->
case x_ap1 of _ {
Bug.T ->
case y_ap2 of _ {
Bug.T -> GHC.Types.True;
Bug.F -> GHC.Types.False;
Bug.Not g1_aBc_ayJ -> GHC.Types.False
};
Bug.F ->
case y_ap2 of _ {
Bug.T -> GHC.Types.False;
Bug.F -> GHC.Types.True;
Bug.Not g1_aBc_ayJ -> GHC.Types.False
};
Bug.Not g1_aBc_ayJ ->
case y_ap2 of _ {
__DEFAULT -> GHC.Types.False;
Bug.Not g1_aBc1_XAu -> Bug.$fGEqLogic_$cgeq g1_aBc_ayJ g1_aBc1_XAu
}
}
end Rec }
</pre><p>
Nice and simple, looking just like what we would expect for an equality function for datatype <tt>Logic</tt>.
</p>
<p>
Now we add one more constructor to datatype <tt>Logic</tt> (and adapt the <tt>Generic</tt> instance accordingly):
</p>
<pre class="wiki">data Logic = T | F
| Not Logic
| And Logic Logic
</pre><p>
GHC (HEAD) now generates 3000 lines of core code for the <tt>Bug.$fGEqLogic_$cgeq</tt> function, instead of something only slightly longer than above.
</p>
<p>
Why is this? The second version of our <tt>Logic</tt> datatype is as easy to optimise as the first version; only the terms involved will be slightly longer. Attached file <tt>Bug2.hs</tt> is the input which gives the correct behaviour, while <tt>Bug3.hs</tt> is the input with one added constructor. (You might wonder if it has to do with the fact that the added constructor has more than one argument, but this is not the source of the problem.) Both files have <tt>INLINE</tt> pragmas pretty much everywhere (in fact, we're not <tt>deriving Generic</tt> so that we can put <tt>INLINE</tt> pragmas on <tt>to</tt> and <tt>from</tt>).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7109#changelog
http://ghc.haskell.org/trac/ghc/ticket/7114
http://ghc.haskell.org/trac/ghc/ticket/7114#7114: Cannot recover (good) inlining behaviour from 7.0.2 in 7.4.1Fri, 03 Aug 2012 13:06:41 GMTdreixel<p>
(I'm sorry that this test case is so large.)
</p>
<p>
The attached module <tt>Code3.hs</tt> is a highly simplified version of a generic implementation of enumeration, followed by its instantiation to a datatype of lists of integers. The goal is to drive the simplifier to fully specialise the generic version to an optimised version for lists, without any reference to the generic representation constructors.
</p>
<p>
With GHC 7.0.2, the (interesting part of the) attached module compiles to the following core code (my renaming):
</p>
<pre class="wiki">enumNil :: [Code2.List]
[GblId, Caf=NoCafRefs]
enumNil =
GHC.Types.: @ Code2.List Code2.Nil (GHC.Types.[] @ Code2.List)
Rec {
lvl1_roO :: GHC.Types.Int -> [Code2.List]
[GblId, Arity=1]
lvl1_roO =
\ (x_XnO :: GHC.Types.Int) ->
GHC.Base.map
@ Code2.List
@ Code2.List
(\ (x1_XnN :: Code2.List) -> Code2.Cons x_XnO x1_XnN)
enumList
lvl2_roR :: [[Code2.List]]
[GblId]
lvl2_roR =
GHC.Base.map
@ GHC.Types.Int @ [Code2.List] lvl1_roO enumInt
enumCons :: [Code2.List]
[GblId]
enumCons = Code2.diag @ Code2.List lvl2_roR
enumList [Occ=LoopBreaker] :: [Code2.List]
[GblId, Str=DmdType]
enumList = Code2.||| @ Code2.List enumNil enumCons
end Rec }
</pre><p>
This is exactly what is intended: no more generic representation stuff. GHC 7.4.1, however, doesn't quite achieve this, instead leaving us with the following:
</p>
<pre class="wiki">enumNil :: [Code2.List]
[GblId, Caf=NoCafRefs]
enumNil =
GHC.Types.: @ Code2.List Code2.Nil (GHC.Types.[] @ Code2.List)
Rec {
a_rme :: [Code2.K1 Code2.List]
[GblId, Str=DmdType]
a_rme =
GHC.Base.map
@ Code2.List
@ (Code2.K1 Code2.List)
(Code2.K1 @ Code2.List)
enumList
lvl1_rmf :: GHC.Types.Int -> [Code2.List]
[GblId, Arity=1]
lvl1_rmf =
\ (x_Xmk :: GHC.Types.Int) ->
GHC.Base.map
@ (Code2.K1 Code2.List)
@ Code2.List
(\ (x1_Xn9 :: Code2.K1 Code2.List) ->
case x1_Xn9 of _ { Code2.K1 b_aaM -> Code2.Cons x_Xmk b_aaM })
a_rme
lvl2_rmg :: [[Code2.List]]
[GblId]
lvl2_rmg =
GHC.Base.map
@ GHC.Types.Int @ [Code2.List] lvl1_rmf enumInt
enumCons :: [Code2.List]
[GblId]
enumCons = Code2.diag @ Code2.List lvl2_rmg
enumList [Occ=LoopBreaker] :: [Code2.List]
[GblId, Str=DmdType]
enumList = Code2.||| @ Code2.List enumNil enumCons
end Rec }
</pre><p>
The strange part is the interaction between the <tt>lvl1_rmf</tt> and <tt>a_rme</tt> functions: basically <tt>a_rme</tt> maps <tt>K1</tt> over a list, and <tt>lvl1_rmf</tt> maps a function that takes this <tt>K1</tt> away.
</p>
<p>
I have no idea why 7.4.1 leaves this residue around. I have played with different inline pragmas and rewrite rules, but so far have been unable to convince GHC 7.4.1 to just do what 7.0.2 did. Turning <tt>K1</tt> into a <tt>newtype</tt> doesn't help (we're left with a newtype coercion instead).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7114#changelog
http://ghc.haskell.org/trac/ghc/ticket/7259
http://ghc.haskell.org/trac/ghc/ticket/7259#7259: Eta expansion of products in System FCFri, 21 Sep 2012 09:18:06 GMTsimonpj<p>
This ticket is to capture the ideas in these GHC-users threads: <a class="ext-link" href="http://www.haskell.org/pipermail/glasgow-haskell-users/2012-August/022790.html"><span class="icon"></span>PolyKinds Aug 2012</a> and <a class="ext-link" href="http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/thread.html"><span class="icon"></span>PolyKinds Sept 2012</a>
</p>
<ul><li>We want to add eta-rules to FC. Sticking to pairs for now, that would amount to adding two new type functions (Fst, Snd), and three new, built-in axioms
<pre class="wiki"> axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
</pre>Generalising to arbitrary products looks feasible.
</li></ul><ul><li>Adding these axioms would make FC inconsistent, because
<pre class="wiki"> axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
</pre>and that has two different type constructors on each side. However, I think is readily solved: see below under "Fixing Any"
</li></ul><ul><li>Even in the absence of Any, it's not 100% obvious that adding the above eta axioms retains consistency of FC. I believe that Richard is volunteering to check this out. Right, Richard?
</li></ul><h2 id="Typeinference">Type inference</h2>
<p>
I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint
</p>
<pre class="wiki"> [W] (a:'(k1,ks)) ~ '( t1, t2 )
</pre><p>
where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint
</p>
<pre class="wiki"> [W] '(Fst a, Snd a) ~ '( t1, t2)
</pre><p>
Is that it? Or do we need more? I'm a bit concerned about constraints like
</p>
<pre class="wiki"> F a ~ e
</pre><p>
where <tt>a:'(k1,k2)</tt>, and we have a type instance like <tt>F '(a,b) = ...</tt>
</p>
<p>
Anything else?
</p>
<p>
I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint
</p>
<pre class="wiki"> [W] a~b
</pre><p>
where <tt>a</tt> and <tt>b</tt> are both skolems of kind <tt>'(k1,k2)</tt>. If we eta-expand both we'll get two insoluble constraints <tt>(Fst a ~ Fst b)</tt> and <tt>(Snd a ~ Snd b)</tt>, and we DEFINITELY don't want to report that as a type error!
</p>
<p>
Someone pointed out that Agda grapples with this problem and we should talk to them.
</p>
<h2 id="FixingAny">Fixing Any</h2>
<ul><li>I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type <strong>family</strong> application on the left and a type constructor on the right.
</li></ul><blockquote>
<p>
I have implemented this change already... it seems like a good plan.
</p>
</blockquote>
<p>
</p>
<ul><li>Several people have asked why we need Any at all. Consider this source program
<pre class="wiki"> reverse []
</pre>At what type should we instantiate <tt>reverse</tt> and the empty list <tt>[]</tt>? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at <tt>(Any *)</tt>:
<pre class="wiki"> reverse (Any *) ([] (Any *))
</pre>Why is Any poly-kinded? Because the above ambiguity situation sometimes arises at other kinds.
</li></ul><ul><li>I'm betting that making Any into a family will mess up Richard's (entirely separate) use of <tt>(Any k)</tt> as a proxy for a kind argument <tt>k</tt>; because now <tt>(Any k1 ~ Any k2)</tt> does not entail <tt>(k1~k2)</tt>. See also the module <tt>GHC.TypeLits</tt> in <tt>base</tt>.
</li></ul><blockquote>
<p>
We can't solve this by making <tt>Any</tt> to be an <em>injective</em> type family, because the use in <tt>TypeLits</tt> uses it in a type-class instance, and you can't match on type families!
</p>
</blockquote>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7259#changelog