[Whoever replies next pl move discussion to haskell-cafe] Bruno Oliveira writes:
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.
Correct. The decomposition law f a = f b ==> a = b applies only to ordinary type constructors (eg list [] etc). See the System FC paper for more details. There's a (silent) constraint imposed on the program
decomp :: f a :=: f b -> a :=: b decomp Eq = Eq
saying that f can only be instantiated with an ordinary type constructor. As far as I know, GHC obeys this restriction (Manuel, Simon and Tom who have implemented type families may be able to tell you more).
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?
As said above, you are not allowed to instantiate f with a type family constructor. Therefore, decomp is fine. The above program text "crashes" becaue we canNOT deduce that K a = K b ==> a =b The decomposition law does NOT apply to type family constructors. Indeed, ghc shouldn't crash here and instead provide a more helpful error message. Martin
Any comments?
Cheers,
Bruno Oliveira _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell