[Haskell-cafe] Type equality proof

[Martijn van Steenbergen]

Martijn van Steenbergen wrote:
>> class Eq2 f where
>>   eq2 :: f a b -> f a' b' -> Maybe (a :=: a', b :=: b')

Is that right, or does the following make more sense?

> class Eq2 f where
>   eq2 :: f a b -> f a' b' -> (Maybe (a :=: a'), Maybe (b :=: b'))

Thanks,

Martijn.