[Haskell-cafe] Type equality proof

[Martijn van Steenbergen]

Olá café,

With the recent generic programming work and influences from 
type-dependent languages such as Agda, the following data type seems to 
come up often:

> data (a :=: a') where
>   Refl :: a :=: a

Everyone who needs it writes their own version; I'd like to compile a 
package with this data type and related utilities, if such a package 
doesn't exist already (I couldn't find one). Below is what I have so 
far; I'd much appreciate it if you added your ideas of what else the 
package should contain.

> {-# 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')

Thank you,

Martijn.