The information on this page is likely out of date. Any updated version will instead appear in the the official user manual
During type checking a metavariable will be generated for each implicit argument.
The metavariables are solved for using a restricted form of pattern unification (1). Basically, a constraint of the form
F x1 .. xn = t for a metavariable
F and distinct variables
x1 .. xn can be solved with
F := \x1 .. xn -> t.
Metavariables in argument positions
Metavariables that appear as arguments to datatypes or constructors have a good chance of being solved. If
D is a datatype then the constraint
D us = D vs is equivalent to
us = vs, which is hopefully solvable for metavariables in
Constructor headed functions
In general when a metavariable appears as an argument to a function defined by pattern matching, the constraint solver will leave the constraint hoping that the metavariable is solved elsewhere. However, for a certain class of functions, which we shall call constructor headed functions, it is possible to do better: If all right hand sides of a function definition have distinct (type or value) constructor heads, we can deduce the shape of the arguments to the function by looking at the head of the expected result. For instance, the following function is constructor headed:
Vec : Set -> Nat -> Set Vec A zero = Unit Vec A (suc n) = Pair A (Vec A n)
Now, if we have a constraint
Vec X Y = Pair s t, for metavariables
Y we can conclude that the only way for
Vec X Y to have the form
Pair _ _ is if the second clause of the definition is chosen, hence we can solve
Y := suc Z for a fresh metavariable
Z and reevaluate the constraint. This results in the constraint
Pair X (Vec X Z) = Pair s t which in turn is reduced to
X = s and
Vec X Z = t.
We can also improve the constraint solving for constraints between two applications of the same constructor headed function. For instance, consider the constraint
Vec s X = Vec t u for a metavariable
X and neutral term
u. If the left hand side reduces it will reduce to a constructor headed term which will not be equal to the right hand side. Hence, the left hand side must be neutral and since neutral applications of a function are equal iff the arguments are equal it must be the case that
s = t and
X = u.
Update (Agda 2.3.2): Agda now expands simple definitions (one clause, terminating) to check whether a function is constructor headed. For instance, the following now also works:
MyPair : Set -> Set -> Set MyPair A B = Pair A B Vec : Set -> Nat -> Set Vec A zero = Unit Vec A (suc n) = MyPair A (Vec A n)
 Unification and anti-unification in the calculus of constructions Frank Pfenning, 1991.