[AnaniasAnanas]

I am pretty sure that the type variable is not binded properly (when type checking App on the part where it says "(Ok (ClosureTy (ctx, Arrow (t0_0, t0_1)))," I get a symbol for t1, you are doing t1 = t0_0 which would be false in any case but the thing is that even when I use lookup in the enviroment I do not find said symbol). I would suggest instead of having closures to replace every occurrence of the type variable (or any variable really) during evaluation. So if you have something like ((\Lambda t (\lambda x t x)) int) to evaluate it into (\lambda x int x) directly instead of (\lambda x (sym "t") x) + a separate environment thing. I can give you my System F implementation in haskell that uses this method if you want.