The Undecidability of System F Typability and Type Checking for Reductionists

The undecidability of both typability and type checking for System F (polymorphic lambda-calculus) was established by Wells in the 1990s. For type checking Wells gave an astonishingly simple reduction from semi-unification (first-order unification combined with first-order matching). For typability Wells developed an intricate calculus to control the shape of type assumptions across type derivatio...