Title: A Direct Algorithm for Type Inference in the Rank 2 Fragment of the Second-Order Lambda-Calculus 
Author: Joe Wells,Boston University 
Date: November 1993


Abstract:

We study the problem of type inference for a family of polymorphic type
disciplines containing the power of Core-ML.  This family comprises all
levels of the stratification of the second-order lambda-calculus by
``rank'' of types.  We show that typability is an undecidable problem at
every rank k >= 3 of this stratification.  While it was already known that
typability is decidable at rank <= 2, no direct and easy-to-implement
algorithm was available.  To design such an algorithm, we develop a new
notion of reduction and show how to use it to reduce the problem of
typability at rank 2 to the problem of acyclic semi-unification.  A
by-product of our analysis is the publication of a simple solution
procedure for acyclic semi-unification.