Tom Hawkins wrote:
data Expr :: * -> * where Const :: a -> Term a Equal :: Term a -> Term a -> Term Bool
Your basic problem is this: p1 :: Term Bool p1 = Equal (Const 3) (Const 4) p2 :: Term Bool p2 = Equal (Const "yes") (Const "no") p1 and p2 have the same type, but you're not going to be able to compare them unless you can compare an Int and a String. What do you want p1 == p2 to do? If you want to just say that different types are always non-equal, the simplest way is to create a witness type for your type-system. For instance: data MyType a where IntType :: MyType Int StringType :: MyType String Now you'll want to declare MyType as a simple witness: instance SimpleWitness MyType where matchWitness IntType IntType = Just MkEqualType matchWitness StringType StringType = Just MkEqualType matchWitness _ _ = Nothing You'll need to include a witness wherever parameter types cannot be inferred from the type of the object, as well as an Eq dictionary: data Term :: * -> * where Const :: a -> Term a Equal :: Eq a => MyType a -> Term a -> Term a -> Term Bool Now you can do: instance Eq a => Eq (Term a) where (Const p1) == (Const p2) = p1 == p2 (Equal w1 p1 q1) (Equal w2 p2 q2) = case matchWitness w1 w2 of MkEqualType -> (p1 == p2) && (q1 == q2) _ -> False -- because the types are different _ == _ = False Note: I haven't actually checked this. Use "cabal install witness" to get SimpleWitness and EqualType. -- Ashley Yakeley