What are the limits of type inference?

Question

What are the limits of type inference? Which type systems have no general inference algorithm?

Answer 1

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.

Answer 2

A value-dependent-type system (Or in short, dependent type system) can describe types that say things like: "At evaluation time (runtime), the value of this variable will always be equal to the value of that variable, which is computed with a different evaluation process". Automatically deducing this type from the code entails automatic proofs of theorems. If the set of theorems you can express is restricted to those automatically provable, that would not be a problem, but in the case of dependently-typed languages, this is generally not the case.

So dependently typed systems cannot have general (and complete) type inference.

I am sure someone can provide a moral formal and complete answer...