Higher-Order Pattern Unification in Agda

Higher-order unification problems can have multiple incompatible
solutions, a challenge for many applications which can't afford to
enumerate nor to guess. A good strategy is instead to defer except for
the cases that fall into the pattern fragment, a subset which
guarantees unique solutions.

The dependently typed programming language Agda, in addition to being
the motivating example for our interest into the subject, proves
itself to be a good tool to formalize the pattern unification
algorithm for the Simply Typed Lambda Calculus, as it was originally
formulated, and its proof of correctness.

Isolating the problem into a precise and modern presentation, we offer
new material for those seeking to understand the benefits and limits
of the solution.