Damas-Milner-like subset of the calculus of constructions with global type inference Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this tradeoff.

Does a similar Damas-Milner-like subset of the calculus of constructions exist, for which global type inference is possible? I expect the answer to be “yes” based on the following clues:


1ML's abstract syntax already unifies terms and types, in a way reminiscent of System Fω's definition as a pure type system, and then makes type inference work for a subset of the language.
AFAICT, Damas-Milner type inference only requires that the type language be first-order, pure, terminating and confluent. First-order unification doesn't require that all unification variables range over a single sort (namely, that of types). A first-order, pure, terminating language can be carved out of a higher-order, effectful, potentially nonterminating language, by means of syntactic restrictions on terms in the latter.


But is there a definitive answer?
As far as I can tell, there is no prime candidate for an analogue of Damas-Milner for CoC. Certainly there is no definitive answer.

Arguably, Damas-Milner isn't even a perfect inference system for $\mathrm{F}_\omega$, as in general it can't infer types with higher kinds in them (though it is an open question as to whether higher kinds are really necessary, see this problem).

At any rate, here's a rather simple argument against a definitive system for the CoC: unification modulo $\beta$ conversion is undecidable in general, even for terms with simple types. But for a given unification problem $t\approx u$ it is rather easy to set up a term which can be typed if and only if $t$ unifies with $u$:

$$ A : \Pi \vec{x}.C\ t\rightarrow \mathrm{nat},\ B:\Pi\vec{x}.C\ u\vdash A\ B$$

where the $\vec{x}$ are the free (unification) variables in $t$ and $u$, as well as the "implicit arguments" which are the analogue of the polymorphic type variables in Damas-Milner.

That being said, there are restrictions of the unification problem which are decidable, most notably Miller patterns which have good properties (uniqueness of solutions), so it's common to restrict implicit argument resolution to Miller patterns and reject the term otherwise.

In practice every dependently typed language does have to solve this problem, if only because giving every single type annotation is unworkably tedious. However, that inference is usually designed to fail in which case the user is asked to supply additional annotations, something which is absent from usual programing language type inference systems.

More background in this cs.stackexchange answer: https://cs.stackexchange.com/questions/12691/what-makes-type-inference-for-dependent-types-undecidable

and this one, more centered on the unification problem:

https://stackoverflow.com/questions/1936432/higher-order-unification

And (tooting my own horn further, I guess), I recommend the article Elaboration in Dependent Type Theory by de Moura et al, as a discussion of the issues involved.