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?