This compiled with today's CVS GHC 6.3. I don't think you can do this without GADTs. module Expression where { data Sym env r where { FirstSym :: Sym (r,xx) r; NextSym :: Sym env r -> Sym (a,env) r }; runSym :: Sym env r -> env -> r; runSym FirstSym (r,xx) = r; runSym (NextSym var) (a,env) = runSym var env; data OpenExpression env r where { Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r); Symbol :: Sym env r -> OpenExpression env r; Constant :: r -> OpenExpression env r; Application :: OpenExpression env (a -> r) -> OpenExpression env a -> OpenExpression env r }; newtype Expression r = MkExpression (forall env. OpenExpression env r); runExpression :: Expression r -> r; runExpression (MkExpression expr) = runOpenExpression expr () where { runOpenExpression :: OpenExpression env a -> env -> a; runOpenExpression (Constant r) _ = r; runOpenExpression (Application ar a) env = (runOpenExpression ar env) (runOpenExpression a env); runOpenExpression (Lambda exp) env = \a -> runOpenExpression exp (a,env); runOpenExpression (Symbol var) env = runSym var env; }; sym0 :: OpenExpression (a,env) a; sym0 = Symbol FirstSym; sym1 :: OpenExpression (a,(b,env)) b; sym1 = Symbol (NextSym FirstSym); sym2 :: OpenExpression (a,(b,(c,env))) c; sym2 = Symbol (NextSym (NextSym FirstSym)); k :: Expression (a -> b -> a); -- k = \x.\y -> x = \.\.1 k = MkExpression (Lambda (Lambda sym1)); s :: Expression ((a -> b -> c) -> (a -> b) -> a -> c); -- s = \x.\y.\z -> x z (y z) = \.\.\.2 0 (1 0) s = MkExpression (Lambda (Lambda (Lambda (Application (Application sym2 sym0) (Application sym1 sym0))))); } -- Ashley Yakeley, Seattle WA