Decidability of rank-k polymorphism vs. System F

Question

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda calculus is undecidable if $k \ge 3$. My thought was that since there must be terms that can be typed in rank-3 but not rank-2, and since System F is rank-$n$ (i.e. the union of all finite rank-$k$), surely this implies that Curry-style System F type inference is undecidable as well. However, its undecidability isn't proven until 1996 by Wells in "Typability and Type Checking in the Second-Order $\lambda$-Calculus Are Equivalent and Undecidable", which explicitly mentions Kfoury's paper (along with others) and states that decidability of both type inference and type checking have not yet been proven until then.

So given that rank-3 polymorphic lambda calculus is a fragment of System F, why doesn't the former's undecidability imply the undecidability of the latter?

Answer 1

The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine):

We prove that [...] for every $k\ge 3$ there is a typing of constants that assigns types in $S(1)$ such that the type reconstruction problem for $\Lambda_k$ extended by this typing is undecidable. Unfortunately, this result does not give any clue as to whether type reconstruction for $F_2$, with or without constants, is decidable. Our decidability/undecidability proofs use in an essential way the apriori information about the rank of types.

So, if you don't force constants to have certain pre-defined types of known rank, or if you don't have constants at all, the problem may become easier (than undecidable). The proofs rely on having constants that are forced to have certain types. (Of course, as you pointed out, Wells showed that the problem isn't easier.)