On the Undecidability of Partial Polymorphic Type Reconstruction

Abstract

We prove that partial type reconstruction for the pure polymorphic λ-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We show further that partial type reconstruction remains undecidable even in a very small predicative fragment of the polymorphic λ-calculus, which implies undecidability of partial type reconstruction for ${\mathit{\lambda }}^{\mathit{M}\mathit{L}}$ as introduced by Harper, Mitchell, and Moggi.