(1994) settled an "embarrassing open problem" by proving that type checking is undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.

Wells's result implies that type inference for System F is impossible.A restriction of System F known as "Hindley-Milner", or simply "HM", does have an easy type inference algorithm and is used for many statically typed