Typability and type checking in the second-order λ-calculus are equivalent and undecidable

The problems of typability and type checking exist for the Girard/Reynolds second-order polymorphic typed λ-calculus (also known as “system F”) when it is considered in the “Curry style” (where types are derived for pure λ-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 λK-calculus and the more restrictive λI-calculus