[Haskell-cafe] A Finally Tagless Pi Calculus

[Dupont Corentin]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100609/cee5888b/attachment.html