Is there a general algorithm to fill holes in terms of the Calculus of Constructions?

Question

Suppose that you extend the Calculus of Constructions with "holes" - i.e., incomplete pieces of code that you didn't fill yet. I wonder if there is an algorithm to fill those roles automatically. For example (using Morte's syntax):

Case A:

λ (pred : ?) 
-> λ (Nat : *) 
-> λ (Succ : Nat -> Nat) 
-> λ (Zero : Nat)
-> (Succ (pred Nat Succ Zero))

On this situation, a type inference algorithm can identify that ? can obviously only be ∀ (Nat : *) -> (Nat -> Nat) -> Nat -> Nat, because pred receives Nat : *, Succ : Nat -> Nat, Zero : Nat, and must return Nat, because it is the first argument of Succ.

Case B:

(Id ? 4)

Where 4 is λ-encoded and Id is the identity function (i.e., ∀ (t:*) -> λ (x:t) -> x). On that situation, ´?´ is again clearly ∀ (N:*) -> (N -> N) -> N -> N, because that is the type of 4.

Case C:

(Id (Equals Nat 7 (add 3 ?)) (Refl 7))

Here,Equals and Refl are defined in a similar fashion to Idris. ? can obviously only be 4, but how do you figure that out? One way would be using the fact that ? : Nat, and Nat is a type which we know how to enumerate, so we can just try all Nats til it typechecks. That can be done for any enumerable type.

Case D:

(Id (Equal Nat 10 (MulPair ?)) 10)

Here, ? can only be of type Pair Nat; it has only more than one valid answer, though: it can be (Pair 10 1), (Pair 2 5), (Pair 5 2) and (Pair 1 10).

Case E:

(Id (Equal Nat 7 (Mul 2 ?)) 7)

Here, there is no valid answer, since 7 isn't a multiple of 2.

---

All those examples made me notice that we can make a general algorithm that identifies some known patterns and gives an answer by handpicking a specific algorithm (type inference, brute-force, and so on), kinda like Wolfram Alpha figures out the right strategy to solve an Integral. But that sounds like an engineering/hardcoded approach. Is there a principled way to solve this problem? Is there any research study/area on it?