The information on this page is likely out of date. Any updated version will instead appear in the the official user manual
Solvable constraints
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.
See talk on the 13th Agda Implementor's Meeting explaining unification in Agda.
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 us or vs.
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 X and 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)
[1] Unification and anti-unification in the calculus of constructions Frank Pfenning, 1991.