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