Hello, I have been playing with ghc6.8.1 and type families and the following program is accepted without any type-checking error:
data a :=: b where Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and ":=:" as equality, then this is saying that if f a = f b then a = b but clearly this does not hold in general. For example: f 1 = 0 f 2 = 0 So, we have that "f 1 = f 2" but this does not imply that "1 = 2". Ofcourse, that before ghc6.8, we add no type-level functions so maybe it was ok to consider the program above. However, with open type functions the following program is problematic and crashes ghc in style:
type family K a
c :: K a :=: K b -> a :=: b c Eq = Eq
with the following error message: ghc-6.8.1: panic! (the 'impossible' happened) (GHC version 6.8.1 for i386-apple-darwin): Coercion.splitCoercionKindOf base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv] <pred>main:Bug.K{tc rom} a{tv aoS} [sk] ~ main:Bug.K{tc rom} b{tv aoT} [sk] It seems to me that the "decomp" should be rejected in the first place? Maybe the fact that "decomp" is accepted is a bug in the compiler? Any comments? Cheers, Bruno Oliveira