[Haskell-cafe] Bug with GADT in function Patterns?

[Manuel M T Chakravarty]

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