Generating constraints to solve dependently-typed metavariables?

Question

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments.

There are many papers which describe, given a unification problem in the pattern fragment, how to find a solution if one exists. Examples include are (Gundry-McBride), (Abel-Pientka), and the original Miller paper.

What I'm wondering is, given a dependently typed program containing metavariables (or implicit arguments), how does one go about generating the problems that are passed to the unification solver?