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
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
