[Haskell] Should the following program be accepted by ghc?

[Bruno Oliveira]

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