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