Unification is the process of solving a set of syntactic equations modulo beta equivalence, binding evars in the process. It is the central engine of the prover. Note that beta equivalence here is understood to include not just the contraction of conventional beta redices, but also all installed reductions, as well as calculations on native terms.

Usually, unification will bind an evar only when that binding is the unique solution to an equation. When an equation is ambiguous (that is, when the solution is not unique), the equation is deferred, in the hope that some other equation resolves the ambiguity.

For example, suppose we have the equation

E[x / y] = x

There are two solutions: E := x and E := y. Thus, the equation is deferred, in the hope that some other equation determines E.

There are two exceptions [1] to this rule:

  1. Consider the equation:

    E x = M x

    where E cannot depend on x. There are two solutions: E := M and E := fn x . M x. These are eta equivalent, but unification recognizes only beta equivalence. (Definitional equality does recognize a form of eta equivalence appropriate to the type in question, but it is not relevant to unification.) Thus, the two solutions are not equivalent. We resolve the ambiguity in favor of the first solution.

  2. Consider the equation:

    E[M / x] = M

    where M is not a variable. There are two solutions: E := M and E := x. We resolve the ambiguity in favor of the first solution.

    (Note that if M is a variable, the equation is deferred as discussed above.)

Failure modes

When unification fails, the variable Unify.errorMessage is set to explain why:

These remaining errors cannot arise from well-typed equations:


Unification is not complete. A system of constraints that has a solution might not be solved, either because of ambiguous constraints, or because one of the two preferences noted above sent unification into a blind alley.

We have seen an example of the former. As an example of the latter, consider:

E x = h x
E = fn x . h x

If the first equation is solved first, then E becomes bound to h, and the second equation becomes h = fn x . h x which fails.

A similar problem arises when unification settles on a non-unique solution (such as E := h above) but another solution was intended and the chosen solution creates problems later on. This is the non-principal solution problem.

Non-principal solutions can be unfortunate because they can lead to confusion for the user. The usual practice in higher-order pattern unification is not to employ them [2]. However, in such settings one usually enjoys eta equivalence. That is not the case here.

In our setting, ruling out non-principal solutions would mean that equations like E x = M x are unsolvable, and such equations happen far too frequently for that to be acceptable.

Equations such as E[M / x] = M are less common, but when they do arise, the E := M solution is intended the vast majority of the time. This is the behavior of every ML typechecker of which we are aware [3]. Having already crossed the Rubicon into non-principal solutions, it seems useful to allow this second sort as well.


On rare occasions, unification may produce the term orphan. This happens when a variable dependency that is being pruned out appears in a term, but not in the term’s normal form. Consider:

E = if true then x else y

where E is not in the scope of y. Pruning succeeds because the right-hand-side’s normal form (x) does not depend on y. However, for performance reasons, Istari does not bind E to the normal form but to a substitution instance of the original right-hand-side:

(if true then x else y)[orphan / y]

(Explicit substitutions usually use much less space than the normal forms of those substitutions, since the unsubstituted term can share space with other occurrences of that term.) When displayed, E is bound to:

if true then x else orphan

In all cases, orphans can be made to disappear by normalizing the term in which they appear.

[1] The claim that all non-principal solutions fall into these two categories is not currently proven. (Nor is it obvious even how to specify the two categories rigorously in general.)

[2] For example, see: Gille Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via Explicit Substitutions: The Case of Higher-Order Patterns. In Joint International Conference and Symposium on Logic Programming, 1996.

[3] To see how such equations arise, see: Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty, and Gabriele Keller. Modular Type Classes. In Thirty-Fourth ACM Symposium on Principles of Programming Languages,

  1. Section 4.6.