[Haskell-cafe] Re: generalised algebraic data types, existential types, and phantom types

[Jim Apple]

I tried to post this to gmane.comp.lang.haskell.general, but it never 
got there - it may belong here anyway.

Abraham Egnor wrote:
 > Is there any closer approximation [of GADTs] possible?

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

data Term a = forall b . (EqType a b, EqType b Int) => Lit Int
             | forall b . (EqType a b, EqType b Int) => Inc (Term Int)
             | forall b . (EqType a b, EqType b Bool) => IsZ (Term Int)
             | If (Term Bool) (Term a) (Term a)
             | forall b . Fst (Term (a,b))
             | forall b . Snd (Term (b,a))
             | forall b c . (EqType a (b,c))=> Pair (Term b) (Term c)

class EqType a b | a->b, b->a
instance EqType a a

Unfortunately, I can't seem to write an eval function:

eval (Lit a) = a

gives

Inferred type is less polymorphic than expected
         Quantified type variable `b' is unified with `Int'
     When checking an existential match that binds
     The pattern(s) have type(s): Term Int
     The body has type: Int
     In the definition of `eval': eval (Lit x) = x

Any ideas?

Jim