GADT regression

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 (closed), 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:

1. 8.1 : OK
2. 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

1. 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

Trac metadata

Trac field	Value
Version	6.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	zunino@di.unipi.it
Operating system	Unknown
Architecture	Unknown