GHC: Ticket #1781: Type equality class leads to non-termination
http://ghc.haskell.org/trac/ghc/ticket/1781
<p>
This program sends the type checker to the land of no return:
</p>
<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
module ShouldCompile where
class E a b | a -> b, b -> a
instance E a a
plus :: (E a (Int -> Int)) => Int -> a
plus x y = x + y
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/1781
Trac 1.0.1chakThu, 18 Oct 2007 07:12:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:1
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:1
<p>
This program was rejected by 6.6.1 with the message
</p>
<pre class="wiki">/Users/chak/Code/haskell/E_Class.hs:10:0:
The equation(s) for `plus' have two arguments,
but its type `Int -> a' has only one
</pre><p>
which is arguably not the right thing to do either.
</p>
<p>
I haven't traced this, but the problem may well be due to an interaction between equality constraints and FDs - at least since I fixed <tt>TcUnify.subFunTys</tt>. The latter function will defer a wanted equality <tt>a ~ (b1 -> b2)</tt>, which in principle would be entailed by the given <tt>E a (Int -> Int)</tt> (with <tt>b1, b2 := Int</tt>). However, the normalisation and entailment machinery for equalities doesn't know about FDs. (I would think that should lead to an error message rather than non-termination, but oh well....)
</p>
<p>
Incidentally,
</p>
<pre class="wiki">module ShouldCompile where
plus :: (a ~ (Int -> Int)) => Int -> a
plus x y = x + y
</pre><p>
works fine.
</p>
<p>
I would expect that this would be fixed as soon as we implement FDs by way of TFs.
</p>
TicketguestSat, 20 Oct 2007 14:17:07 GMTseverity changed; cc, milestone set
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:2
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:2
<ul>
<li><strong>cc</strong>
<em>g9ks157k@…</em> added
</li>
<li><strong>severity</strong>
changed from <em>normal</em> to <em>blocker</em>
</li>
<li><strong>milestone</strong>
set to <em>6.8.1</em>
</li>
</ul>
<p>
I set the milestone to 6.8.1 and the severity to blocker, and I hope for your understanding. The reason is that at the moment it seems to be impossible to implement a HList-like equality test. At some point you need a type equality constraint, either <tt>t1 ~ t2</tt> or <tt>E t1 t2</tt> (with <tt>E</tt> being defined as above). But neither of them works! The latter doesn’t work because of this very bug, the former doesn’t work probably because of bug <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1754" title="bug: Border case type families/type equality coercions cause the impossible to ... (closed: fixed)">#1754</a>. So if GHC 6.8.1 is released without this bug being fixed I’ll probably have to tell my users (of Grapefruit) that they need something like GHC 6.8.0.20070916. :-(
</p>
TicketguestSat, 20 Oct 2007 14:26:27 GMT
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:3
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:3
<p>
Oh, I should have added that I currently use GHC 6.8.0.20071019 and that this suffers from the bug.
</p>
TicketrossSat, 20 Oct 2007 15:50:16 GMTmilestone deleted
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:4
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:4
<ul>
<li><strong>milestone</strong>
<em>6.8.1</em> deleted
</li>
</ul>
<p>
Milestone is for those who intend to fix the bug.
</p>
TicketchakMon, 22 Oct 2007 07:16:01 GMTseverity changed
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:5
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:5
<ul>
<li><strong>severity</strong>
changed from <em>blocker</em> to <em>normal</em>
</li>
</ul>
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/1781#comment:2" title="Comment 2 for Ticket #1781">guest</a>:
</p>
<blockquote class="citation">
<p>
I set the milestone to 6.8.1 and the severity to blocker, and I hope for your understanding. The reason is that at the moment it seems to be impossible to implement a HList-like equality test. At some point you need a type equality constraint, either <tt>t1 ~ t2</tt> or <tt>E t1 t2</tt> (with <tt>E</tt> being defined as above). But neither of them works! The latter doesn’t work because of this very bug, the former doesn’t work probably because of bug <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1754" title="bug: Border case type families/type equality coercions cause the impossible to ... (closed: fixed)">#1754</a>. So if GHC 6.8.1 is released without this bug being fixed I’ll probably have to tell my users (of Grapefruit) that they need something like GHC 6.8.0.20070916. :-(
</p>
</blockquote>
<p>
You may have misunderstood the problem exposed by this bug - maybe my explanation just wasn't clear. The problem is <strong>not</strong> with the equality class <tt>E</tt> as such. It's with this particular use in the definition of <tt>plus</tt>, where the signature type contains a type variable that is constrained to be a function by the class context. This is something that has <strong>never</strong> worked in GHC, so I doubt that it breaks any existing code.
</p>
<p>
Having said that, maybe you found some other problems with <tt>E</tt>. Then, please document them in a separate bug (if you haven't yet). In any case, this particular bug is surely no blocker, in fact it is fairly obscure and I'd doubt anybody is going to run into it.
</p>
TicketguestMon, 22 Oct 2007 20:42:53 GMT
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:6
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:6
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/1781#comment:5" title="Comment 5 for Ticket #1781">chak</a>:
</p>
<blockquote class="citation">
<p>
You may have misunderstood the problem exposed by this bug - maybe my explanation just wasn't clear. The problem is <strong>not</strong> with the equality class <tt>E</tt> as such. It's with this particular use in the definition of <tt>plus</tt>, where the signature type contains a type variable that is constrained to be a function by the class context. This is something that has <strong>never</strong> worked in GHC, so I doubt that it breaks any existing code.
</p>
</blockquote>
<p>
As I understand, this code didn’t make the type checker loop in previous versions of GHC. So maybe there is a new problem in GHC which causes the looping of the type checker in this case, and this problem could also cause the looping with my code.
</p>
<p>
But since you want so, I will file a new bug report. :-)
</p>
TicketsimonpjWed, 24 Oct 2007 13:15:41 GMT
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:7
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:7
<p>
OK, we'll park this one until <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1795" title="bug: typechecker loops on simple program with fundep (closed: fixed)">#1795</a> and <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1797" title="merge: type equality test leads to a looping type checker (closed: fixed)">#1797</a> are dealt with. (I agree there's a bug here.)
</p>
<p>
Simon
</p>
TicketsimonpjSat, 27 Oct 2007 16:10:41 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:8
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:8
<ul>
<li><strong>testcase</strong>
set to <em>FD1</em>
</li>
</ul>
TicketsimonpjSat, 27 Oct 2007 16:43:41 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:9
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:9
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Thank you for the report. I've fixed this one -- or at least I have restored the same behaviour as 6.6 had for fundeps. In particular the type checker does not loop.
</p>
<p>
Arguably this one should pass, because of the type equality, but that's not going to happen until we have the full glory of type equalities implemented.
</p>
<p>
Simon
</p>
TicketsimonpjSat, 27 Oct 2007 16:44:43 GMT
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:10
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:10
<p>
Oh, the fix is this patch:
</p>
<pre class="wiki">Sat Oct 27 16:54:59 GMT Daylight Time 2007 simonpj@microsoft.com
* Make 'improvement' work properly in TcSimplify
</pre>
TicketsimonmarTue, 30 Sep 2008 15:40:23 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:11
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:11
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:32 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:12
http://ghc.haskell.org/trac/ghc/ticket/1781#comment:12
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket