Tom Hawkins wrote:
apfelmus wrote:
So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that:
(===) :: Expr a -> Expr b -> Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' && b === b' _ === _ = False
instance Eq (Expr a) where (==) = (===)
OK. But let's modify Expr so that Const carries values of different types:
data Expr :: * -> * where Const :: a -> Term a Equal :: Term a -> Term a -> Term Bool
How would you then define:
Const a === Const b = ...
Well, Const :: a -> Term a is too general anyway, you do need some information on a to be able to compare different Const terms. An Eq constraint on a is the minimum: Const :: Eq a => a -> Term a But that's not enough for (===) of course, additional information as suggested by others is needed. Regards, apfelmus