# Finding The Values Of Implicit Arguments

### 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.