[Haskell-cafe] lambda evaluator in GADT

[paul at theV.net]

The introduction to GADT usually starts with a little expression
evaluator. So I gave it a try, but there are some troubles. 

A little data type for lambda expression

> data E a where
>   Lit :: a -> E a
>   App :: E (a -> b) -> E a -> E b
>   Lam :: Var a -> E b -> E (a -> b)
>   Val :: Var a -> E a
>
> data Var a = Var String

some sample values

> e1 = Lit 1
> plus = Lit (\x y -> x + y)

Next, plus' demonstrate a pitfall in my data definition,
i.e., the variable introduced by Lam has type forall a . a,
which is is too general force a constraint on its
occurrances. I wonder if there a way to make it work. 

> plus' = let v1 = Var "x"
>             v2 = Var "y"
>          in Lam v1 (Lam v2 (App (App plus (Val v1)) (Val v2)))

evaluation

> eval :: E a -> a
> eval (Lit x) = x
> eval (App f x) = (eval f) (eval x)
> eval (Lam (Var v) e) = \x -> eval (sub v (Lit x) e)
> eval (Val (Var v)) = undefined

substituation

> sub :: String -> E b -> E c -> E c
> sub v e e1@(Lit x) = e1
> sub v e (App f x) = App (sub v e f) (sub v e x)
> sub v e e'@(Lam w'@(Var w) x) =
>       if v == w then e'
>                  else Lam w' (sub v e x)

the above all works fine, except for the following

> {--
> sub v e e'@(Val (Var w)) =
>       if v == w then e
>                 else e'
> --}

It seems the last case requires a unification 
of b and c, which is simply too strong for other
cases. What should I do here?

Instead of substituting on term level, an alternative
way to implement eval is to use an environment to
map variables to its values, but that requires all
expression values to have a uniform type, which is
a conflict to GADT. I'm sure this could be a common
issue encountered by GADT beginners, how does one
get around it?

One solution on top of my head is to use a sum type
(or even type class) and stuff every possible value
types under it, but that defeats the purpose of 
using GADT in the first place.

Any help is greatly appreciated!

Regards,
Paul Liu