Type inference and extensionality

The polymorphic type assignment system F₂ is the type assignment counterpart of Girard´s and Reynolds´ (1972) system F. Though introduced in the early seventies, both the type inference and the type checking problems for F₂ remained open for a long time. Recently, an undecidability result was announced. Consequently, it is considerably interesting to find decidable restrictions of the system. We show a bounded type inference and a bounded type checking algorithm, both based on the study of the relationship between the typability of a term and the typability of terms that “properly” η-reduce to it