Is there a general algorithm to fill holes in terms of the Calculus of Constructions?
There is certainly a lot of research into this problem! It often goes by the name of elaboration. It is an undecidable problem in general, as you may have guessed. The "holes" are often called meta-variables or unification variables.

As I explain a bit in this answer, the problem reduces to higher order unification, on which several people have written whole PhD dissertations.

As you note in your examples, some cases are somewhat easy, and can be solved by the application of simple rules, whereas some seem significantly more difficult, and have more of a "theorem proving" feel to them.

A third possible case is a "type class" type problem, where ? represents some kind of structure, such as a group or field structure, as in

mul ? 2 3


with mul : forall G:Group, G.carrier -&gt; G.carrier -&gt; G.carrier or some variant. Here we need to find a G such that G.carrier == nat.

In general, you want to have 3 different "regimes" for each type of problem, the simple unification, theorem proving, and type class resolution problems respectively.

We explain this a bit in the following paper:

Elaboration in Dependent Type Theory, de Moura, Avigad, Kong &amp; Roux.

You might want to look at the references of that paper for more info.



I've you've got a strong stomach, here is the open-source for elaboration in Lean.

Here is a wiki post that describes the interface to the elaborator in Idris.