[Haskell-cafe] Type equality proof

[Brent Yorgey]

On Tue, Mar 17, 2009 at 11:39:05AM +0100, Martijn van Steenbergen wrote:
>
>> {-# LANGUAGE GADTs #-}
>> {-# LANGUAGE TypeOperators #-}
>> module Eq where
>> data (a :=: a') where
>>   Refl :: a :=: a
>> class Eq1 f where
>>   eq1 :: f a -> f a' -> Maybe (a :=: a')
>> class Eq2 f where
>>   eq2 :: f a b -> f a' b' -> Maybe (a :=: a', b :=: b')
>> class Eq3 f where
>>   eq3 :: f a b c -> f a' b' c' -> Maybe (a :=: a', b :=: b', c :=: c')
>

I don't understand your classes Eq1, Eq2, and Eq3.  How would you make
an instance of Eq1 for, say, [] ?

  instance Eq1 [] where
    eq1 xs ys = ???

It seems you are confusing _value_ equality with _type_ equality?  A
value of type a :=: a' is a proof that a and a' are the same type.
But given values of type f a and f a', there is no way to decide
whether a and a' are the same type (no matter what f is), since types
are erased at runtime.

Maybe you mean for eq1 to have a type like 

  eq1 :: (f a :=: f a') -> (a :=: a')  ?

But actually, you don't need a type class for that either; 

  eq1 :: (f a :=: f a') -> (a :=: a')
  eq1 Refl = Refl

type checks just fine.

-Brent