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?