GHC: Ticket #2040: GADT regression
http://ghc.haskell.org/trac/ghc/ticket/2040
<p>
The following compiles fine in 6.8.1 but does not in later versions of GHC.
</p>
<p>
I'm not sure if this is related to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1823" title="#1823: bug: GADTs and scoped type variables don't work right (closed: fixed)">#1823</a>, since there type classes are not involved.
</p>
<p>
A workaround is included below.
</p>
<pre class="wiki">{-# OPTIONS_GHC -Wall -fglasgow-exts #-}
module Bug where
data Teq a b where Teq :: Teq a a
class C a b where proof :: Teq a b
data S a = S a
data W b where
-- This would make every version of GHC happy
-- W :: (C a c , c ~ S b) => W a -> W c
W :: C a (S b) => W a -> W (S b)
foo :: W (S ()) -> W (S ()) -> ()
foo (W (_ :: W a1)) (W (_ :: W a2)) =
case proof :: Teq a1 (S ()) of
Teq -> ()
foo2 :: W (S ()) -> W (S ()) -> ()
foo2 (W (_ :: W a1)) (W (_ :: W a2)) =
case proof :: Teq a1 (S ()) of
Teq -> case proof :: Teq a2 (S ()) of
Teq -> ()
</pre><p>
Results:
</p>
<p>
6.8.1 : OK
</p>
<p>
6.8.2 : foo OK, foo2 FAIL
</p>
<pre class="wiki">Bug.hs:23:16:
Could not deduce (C a1 (S ())) from the context ()
arising from a use of `proof' at Bug.hs:23:16-20
</pre><p>
6.9.20080108 : FAIL
</p>
<pre class="wiki">Bug.hs:16:7:
Could not deduce (C a (S ()))
from the context (S () ~ S b1, C a1 (S b1))
arising from a use of `proof' at Bug.hs:16:7-11
Bug.hs:21:7:
Could not deduce (C a (S ()))
from the context (S () ~ S b1, C a1 (S b1))
arising from a use of `proof' at Bug.hs:21:7-11
Bug.hs:22:16:
Could not deduce (C a1 (S ())) from the context (S () ~ a)
arising from a use of `proof' at Bug.hs:22:16-20
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2040
Trac 1.2.2.dev0simonpjWed, 16 Jan 2008 12:40:21 GMTowner, difficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:1
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
<p>
Thanks for a good report.
</p>
<p>
Having looked at the code, I think it's quite surprising that 6.8.1 worked at all. Just for the record (I don't expect users to understand this bit), the problem is this. Here's a smaller version of the code, decorated with constraints:
</p>
<pre class="wiki">foo2 :: W (S ()) -> W (S ()) -> ()
foo2 (W (_ :: W a1)) -- C a1 b1, S () ~ S b1
(W (_ :: W a2)) -- C a2 b2, S () ~ S b2
=
case {-# Needs C a1 (S ()) #-}
proof :: Teq a1 (S ()) of
Teq -> {-# Provides a1~S () #-}
{-# Needs: C a2 (S ()) #-}
(proof :: Teq a2 (S ()))
`seq` ()
</pre><p>
The inner use of <code>proof</code> gives rise to a constraint <code>(C a2 (S ()))</code>. This is wrapped in an implication constraint because of the enclosing case expression. But the <code>tci_reft</code> of that implication constraint does not include the type refinements from the enclosing pattern matches. So when <code>reduceImplication</code> makes that the current type refinement, we're missing the outer refinements.
</p>
<p>
This is a clear bug in 6.8.2, since there is no use of type functions. It would in principle be fixable in 6.8.3, but it's not completely trivial to do, so I'm disinclined to attempt it since we are rejigging the whole machinery for the HEAD.
</p>
<p>
Meanwhile the HEAD falls over (which it should not) because the constraint simplifier is not deducing all the things it should. This is Manuel's pigeon at the moment, so I'm assigning the bug to him. In due course this program should join the test suite.
</p>
<p>
Simon
</p>
TicketchakMon, 29 Sep 2008 07:36:11 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:2
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>T2040</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Fine with new solver.
</p>
TicketsimonmarTue, 30 Sep 2008 15:40:30 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:3
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:39 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2040#comment:4
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket