Higher-Order Dynamic Pattern Unification for Dependent Types and Records

While higher-order pattern unification for the lambda(Pi)-calculus is decidable and unique unifiers exists, we face several challenges in practice: 1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification algorithm. 2) Many systems implement lambda(Pi Sigma) calculus and hence the known pattern unification algorithms for lambda(Pi) are too restrictive. In this paper, we present a constraint-based unification algorithm for lambda(Pi Sigma)-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing Sigma-types into problems only involving Pi-types. We prove correctness of our algorithm and discuss its application.