type signatures with existentially quantified data constructors

[Avi Pfeffer]

Hi all,

I'm trying to write an interpreter for a language embedded in Haskell,
that "inherits" Haskell types and values.  So I create a type Expr a, to
represent expressions of type a, and an evaluator that takes an Expr a
and produces an a.  (To keep things simple, let's assume there are no
variables.)   I start with

data Expr a = Haskell a
            | If (Expr Bool) (Expr a) (Expr a) 

eval :: Expr a -> a 
eval (Haskell x) = x 
eval (If x y z)  = if eval x then eval y else eval z

Next, applications.  To correctly type an application expression, I need
to introduce an existentially quantified type variable:  

data Expr a = ... | forall b . Appl (Expr (b->a)) (Expr a)

eval (Appl x y) = (eval x) (eval y)

Works fine.  Things get tricky when I try to add pairs.  In order to type
a pair expression, I find I need to create a Pair class and introduce a 
class constraint:

class Pair a b c | a -> b c, b c -> a 

instance Pair (b,c) b c 

data Expr a = ... | forall b c . Pair a b c => MkPair (Expr b) (Expr c)

This seems to express the right type relationships.  But now I find I
can't write eval for MkPair:

eval (MkPair x y) = (eval x, eval y)

GHC produces the error message

    Cannot unify the type-signature variable `a'
        with the type `(t, t1)'
        Expected type: a
        Inferred type: (t, t1)
    in the definition of function `eval': (eval x, eval y)

I have tried various ways of adding type annotations, but I can't seem to
make it work.  The problem seems to be the combination of class constraint
with existential variables.  How can I tell the compiler that it should in
fact unify a with (t,t1) here?  Or am I misunderstanding something, and
there is a reason it can't?  Perhaps there's a way of typing MkPair
without introducing the Pair class?  Or is there a completely different
approach to my problem?  All suggestions welcome.

--Avi