The first reason mentioned is suspicious: "undecidable, as type checking in System F is undecidable". For a properly annotated version of System F (Church-style), type checking is decidable, while type inference is not. For Curry-style System F, both are undecidable.
Thanks for the clarification. I've removed mentions to System F, as the other links are already provide sufficient reasons.