Incidentally I did find a solution that fits into the type system and also produces the correct result. This was done by making the global parameter change type as well at each lambda so that it becomes a function with the same arrity as the term. Unfortunately to evaluate these terms the program needs fork and do redundant work at every application of lam (so it's a major hack), though it does give me some confidence that a real solution is possible perhaps by using dependent types?:

----

lam :: ((g->(g,a)) -> (g->(g',b))) -> (g->(a->g',a->b))

lam = (\ f -> \ g -> (\x -> fst $ (f (\ gv->(gv,x))) g,

\y -> snd $ (f (\ gv->(gv,y))) g ))

app :: (g->(a->g1,a->b)) -> (g->(g,a)) -> (g->(g1,b))

app = (\ eA eB -> \ gz -> let (gB, fB) = eB gz

in let (lgA, lfA) = eA gB

in (lgA fB, lfA fB) )

ext :: ((g1,a)->(g2,b))->(g0->(g1,a))->(g0->(g2,b))

ext = \f -> \a -> \g -> f (a g)

idCounter :: Num g => (g,a) -> (g, a)

idCounter = \(g, x) -> (g+1, x)

-- Example terms

trmA = lam (\x -> lam (\y -> app x y))

trmB = (lam (\y -> app trmC y))

trmC = (\g -> (\c->g,\c->c+3))

trmD = (\g -> (g,3))

trmE = app trmC trmD

trmF = (ext idCounter) trmD

trmG = app trmC (app trmC trmF)

trmH = app trmC trmE

---

Here's my original statement of the problem http://hastebin.com/raw/bewiqihiyo

And here's all my code with new, http://hpaste.org/86273

Unfortunately, I don't know of a way to tell the compiler that essentially the variables x and y in the lam function will always be applied to the same value. Unfortunately, I've reached a limit of my understanding of how pairs integrate with the type system in Haskell,

I've considered returning something other than a pair from my base function (such as a function) but I have yet to figure that out.

Thanks for your insights,

Ian Bloom