Hi guys, 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? Cheers, hugo