Hi Hugo,
I have found a bug on the compiler (at least ghc >6.8.2). For some module (yes, the example does nothing at all):
module Test where
data Type a where Func :: Type a -> Type b -> Type (a -> b) PF :: Type a -> Type (PF a)
data PF a where ID :: PF (a -> a)
test :: Type a -> a -> a test (PF (Func _ _)) ID = ID
I get the impossible:
$ ghci Test.hs -fglasgow-exts GHCi, version 6.9.20080303: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. [1 of 1] Compiling Test ( Test.hs, interpreted ) ghc-6.9.20080303: panic! (the 'impossible' happened) (GHC version 6.9.20080303 for i386-apple-darwin): Coercion.splitCoercionKindOf $co${tc aog} [tv] <pred>t_ao8{tv} [tau] ~ a{tv aob} [sk] -> a{tv aob} [sk] Please report this as a GHC bug: http://www.haskell.org/ghc/ reportabug
However, the following implementations of test compile ok:
test :: Type a -> a -> a test (PF _) ID = ID
test :: Type a -> a -> a test (PF (Func _ _)) x = x
It has something to do with mixing different GADTs contructors.
Should this be submitted as a bug as it is?
The implementation of type checking of GADTs was completely redone in 6.9. Could you please check whether you have the same problem with the current version of 6.9 in the darcs repo. If yes, then please submit it as a bug. Thanks, Manuel