id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
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,,Unknown,T2040,,,