[lifthrasiir]

As far as I see, you don't really seem to even try to infer types. With fixes to `string_of_*` routines (yeah, some cases are missing) the particular failure is as follows:

    ty(TApp ...) = Closure (Arrow (SymbolTy a) (Arrow (SymbolTy _b) (SymbolTy a)))
    ty(Int 1) = IntTy
    ty(App (TApp ...) (Int 1)) = Failure
      "Type mismatch. t0_0: SymbolTy a, t0_1: Arrow (SymbolTy _b) (SymbolTy a), t1: IntTy".

Here `t0_0` is a formal argument type and `t1` is being applied, so even though they are structurally different it should be inferred that `SymbolTy a` equals to `IntTy` (probably by updating the context). But your code doesn't do that.

I strongly recommend to first familize yourself with Hindley-Milner type system (and possibly Algorithm W) which type inference is efficient and easy enough to understand. Even though the decidable type inference in System F is impossible, the basic techniques for (partial) type inference are not too different.