Skip to content

GitLab

GHC
GHC
Closed
Opened by hpacheco@trac-hpacheco

GADTs in function Patterns

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

NOTE: This same code used to work fine in ghc 6.6, but I have ben told the whole GADT type checing was redone in 6.9. However, with 6.8.2 I still get the same error.

Edited by Simon Peyton Jones