id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential
2040,GADT regression,guest,chak,"The following compiles fine in 6.8.1 but does not in later versions of GHC.
I'm not sure if this is related to #1823, since there type classes are not involved.
A workaround is included below.
{{{
{-# 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 -> ()
}}}
Results:
6.8.1 : OK
6.8.2 : foo OK, foo2 FAIL
{{{
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
}}}
6.9.20080108 : FAIL
{{{
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
}}}",bug,closed,normal,6.10 branch,Compiler (Type checker),6.8.2,fixed,gadt,zunino@…,Unknown/Multiple,Unknown/Multiple,,T2040,,,,