On Wednesday 09 June 2010 2:32:29 pm Dupont Corentin wrote:
I am making a little GATD:
{-# LANGUAGE GADTs#-}
data Obs a where
Equal :: Obs a -> Obs a -> Obs Bool Plus :: (Num a) => Obs a -> Obs a -> Obs a
(etc..)
instance Show t => Show (Obs t) where
show (Equal a b) = (show a) ++ " Equal " ++ (show b) show (Plus a b) = (show a) ++ " Plus " ++ (show b)
instance Eq t => Eq (Obs t) where
a `Equal` b == c `Equal` d = (a == c) && (b == d) a `Plus` b == c `Plus` d = (a == c) && (b == d)
Your two symptoms have the same underlying cause. The 'a' in Equal is existentially quantified. It might help to think about bundling the type in the Equal constructor: Equal T x y :: Obs Bool where T :: * x :: Obs T y :: Obs T Now we write: show (Equal T x y) = ... but we have no evidence that (Show T), so we cannot conclude (Show (Obs T)), and thus cannot use show on x and y. Similarly: Equal T x y == Equal T' x y = ... Your definition assumes that T = T' (or, it assumes that Obs T = Obs T', but that reduces to T = T'), but we have no reason to suspect that is the case. Hence the mismatch. The first can be solved by putting a Show constraint on the type of the Equal constructor, if that's what you really want. The second can probably only be solved by having Equal take some kind of type rep, and checking that the types are equal. Hope that helps. -- Dan