A higher-order unification algorithm is an essential component of a dependently typed programming language implementation, and understanding its capabilities is important if dependently typed programmers are to become productive. Miller showed that, for simply typed λ-terms in the pattern fragment (where metavariables are applied to spines of distinct bound variables), unification is decidable and most general unifiers exist. We describe an algorithm for pattern unification in a full-spectrum dependent type theory with dependent pairs (Σ-types). The algorithm exploits heterogeneous equality and a novel concept of 'twin' free variables to handle dependency. Moreover, it supports dynamic management of constraints, postponing equations that fall outside the pattern fragment in case other equations make them simpler. We aim to make sense both to language implementors and users, and to this end present our algorithm as a Haskell program.
Important note: if you are interested in this paper, you may be better off reading chapter 4 of my thesis, which presents this material more thoroughly. On the other hand, the paper is substantially more compact. There is an error in the description of pruning (in both the paper and thesis), described in the thesis errata.
Latest version: A tutorial implementation of dynamic pattern unification (PDF), updated 10th July 2012, rejected from POPL 2013
Haskell code: download the source tarball or view code from thesis on GitHub