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

[J.N. Oliveira]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3082 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell/attachments/20080116/530dccc8/smime-0001.bin