Hello, 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)
The Equal constructor causes me problems, while the Plus is fine: test3.lhs:8:26: Could not deduce (Show a) from the context (t ~ Bool) arising from a use of `show' at test3.lhs:8:26-31 Possible fix: add (Show a) to the context of the constructor `Equal' In the first argument of `(++)', namely `(show a)' In the expression: (show a) ++ " Equal " ++ (show b) In the definition of `show': show (Equal a b) = (show a) ++ " Equal " ++ (show b) I guess this is because GADT refines type with pattern matching. Since Equal return type is Obs Bool and not Obs a, it cannot bind the type variable a to belong to Show. I don't see how to precise the type in the pattern match. I have another problem: test3.lhs:12:41: Couldn't match expected type `a' against inferred type `a1' `a' is a rigid type variable bound by the constructor `Equal' at test3.lhs:12:8 `a1' is a rigid type variable bound by the constructor `Equal' at test3.lhs:12:23 Expected type: Obs a Inferred type: Obs a1 In the second argument of `(==)', namely `c' In the first argument of `(&&)', namely `(a == c)' Cheers, Corentin