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

On Jan 16, 2008, at 2:08 AM, Bruno Oliveira wrote:

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

This is saying that f is injective. So perhaps the standard interpretation leads implicitly to this class of functions. Cheers jno