What are the limits of type inference? Which type systems have no general inference algorithm?
Joe Wells showed that type inference is undecidable for System F, which is the most basic polymorphic lambda calculus, independently discovered by Girard and Reynolds. This is the most important result showing the limits of type inference.
Here's an important problem that is still open: what is the best way to integrate Generalized Algebraic Data Types into Hindley-Milner type inference? Every year Simon Peyton Jones comes up with a new answers, which is supposedly better than the previous year's answer. I haven't read the March 2009 version and so can't say if I believe it will be definitive.