Type reconstruction in finite rank fragments of the second-order λ-calculus
Assaf J. Kfoury, Jerzy Tiuryn · Information and Computation · 1992
The prove that the problem of type reconstruction in the polymorphic λ-calculus of rank 2 is polynomial-time equivalent to the problem of type reconstruction in ML, and is therefore DEXPTIME-complete. We also prove that for every k > 2, the problem of type reconstruction in the polymorphic λ-calculus of rank k, extended with suitably chosen constants with types of rank 1, is undecidable.