Is there a simple algorithm for proof search on CoC? Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/elegant algorithm capable of solving this problem for a large class of terms? For example, given the term below:

λ (N : Type)
λ (S : {x : N} N)
λ (Z : N)
λ (A : {x : N} Type)
λ (B : {x : N} (A x))
λ (C : {x : (A (S (S (S Z))))} Type)
(C _)


The algorithm would replace _ by (B (S (S (S Z)))),  as it is the only substitution that makes the resulting term well-typed. I'm specifically looking for keywords / references, as I believe this is a pretty well-researched subject (given that most theorem provers feature proof search), but I've never seen an algorithm described in a simpler setup (like plain CoC).
Is there a simple algorithm? yes. Simply enumerate all possibilities.  Of course this is pretty intractable in practice.

A proper sub-problem of term generation in CoC is "higher-order unification".  It handles the simply typed lambda calculus.  It is undecidable.  But there is a classic practical solution by Huet.  There are a lot of resources here: https://stackoverflow.com/questions/1936432/higher-order-unification.

Now the only good reference I know for CoC term generation is "A Complete Proof Synthesis Method for the Cube of Type Systems" by Dowek.  I believe this summarizes his thesis work (in french) and there is a draft pdf floating around (it has some errors).  His r-splitting construction is a little awkward for implementations, but he does a good job of highlighting the difficulties, and suggesting practical in-complete solutions.