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

[Bruno Oliveira]

Hello,

Maybe a more slightly more honest type for "decomp" would be:) :

decomp :: Injective f => f a :=: f b -> a :=: b

Cheers,

Bruno

On Wed, 16 Jan 2008, Derek Elkins wrote:

> On Wed, 2008-01-16 at 09:18 +0000, J.N. Oliveira wrote:
>> 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.
>
> Just like data constructors, type constructors are injective. f a
> doesn't simplify and so essentially you have structural equality of the
> type terms thus f a = f b is -equivalent- to a = b.  Obviously type
> functions change this, just like normal value functions do at the value
> level.
>
>