Type inference and extensionality

The polymorphic type assignment system F/sub 2/ 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/sub 2/ 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" /spl eta/-reduce to it. >