Parameter-free polymorphic types

Consider the following restriction of the polymorphically typed lambda calculus (“System F ”). All quantifications are parameter free. In other words, in every universal type ∀ α . τ , the quantified variable α is the only free variable in the scope τ of the quantification. This fragment can be locally proven terminating in a system of intuitionistic second-order arithmetic known to have strength of finitely iterated inductive definitions.