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