What makes type inference for dependent types undecidable?

Question

I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit of "dependency" where types can be indexed by values, below which type inference is possible and above which it is not?

Answer 1

For a rather simple version of dependent type theory, Gilles Dowek gave a proof of undecidability of typability in a non-empty context:

Gilles Dowek, The undecidability of typability in the $\lambda\Pi$-calculus

Which can be found here.

First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the abstractions, it is undecidable to show typeability of a term in a non-empty context. Both of those hypotheses are necessary: in the empty context, typability reduces to that of the simply-typed $\lambda$-calculus (decidable by Hindley-Milner) and with the annotations on the abstractions, the usual type-directed algorithm applies.

The idea is to encode a Post correspondence problem as a type conversion problem, and then carefully construct a term which is typeable iff the two specific types are convertible. This uses knowledge of the shape of normal forms, which always exist in this calculus. The article is short and well-written, so I won't go into more detail here.

Now in polymorphic calculi like system-F, it would be nice to be able to infer the type abstractions and applications, and omit the annotations on $\lambda$s as above. This is also undecidable, but the proof is much harder and the question was open for quite some time. The matter was resolved by Wells:

J. B. Wells, Typability and type checking in System F are equivalent and undecidable.

This can be found here. All I know about it is that it reduces the problem of semi-unification (which is unification modulo instantiation of universal quantifiers, and is undecidable) to type checking in System F.

Finally it is quite easy to show that inhabitation of dependent families is undecidable: simply encode a Post problem into the constructor indices. Here are some slides by Nicolas Oury that sketch the argument.

As to whether there is a "limit", it much depends on what you are trying to do with your dependent types, and there are many approximations which try to be either decidable, or at least close enough to be usable. These questions are still very much part of active research though.

One possible avenue is the field of "refinement types" where the language of expression of type dependencies is restricted to allow for decidable checking see, e.g. Liquid Types. It's rare that full type inference is decidable even in these systems though.