# [Haskell-cafe] A Finally Tagless Pi Calculus

Dupont Corentin corentin.dupont at gmail.com
Wed Jun 9 14:32:29 EDT 2010

```Hello,
I am making a little GATD:

> 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...