Typability and type checking in the second-order λ-calculus are equivalent and undecidable
J. B. Wells · 2002
The problems of typability and type checking exist for the Girard/Reynolds second-order polymorphic typed /spl lambda/-calculus (also known as "system F") when it is considered in the "Curry style" (where types are derived for pure /spl lambda/-terms). Until now the decidability of these problems for F itself has remained unknown. We first prove that type checking in F is undecidable by a reduction from semi-unification. We then prove typability in F is undecidable by a reduction from type checking. Since the reduction from typability to type checking in F is already known, the two problems in F are equivalent (reducible to each other). The results hold for both the usual /spl lambda/K-calculus and the more restrictive /spl lambda/I-calculus.>