Extended Abstract: From Pattern Unification Towards Pattern Matching Unification
David Richter, Timon Böhler
cs.PL
Jul 20, 2026 · v1
TL;DR
A prototype dependently typed language integrating pattern matching into unification was implemented in under 3000 lines of Lean.
Abstract
We revisit the role of higher-order unification in dependently typed languages and identify a fundamental limitation of existing pattern-based fragments: their inability to synthesize functions defined by case analysis. Even simple and ubiquitous constraints arising from type inference, particularly from use of induction principles, fall outside the expressive power of Miller patterns and their modern extensions. We observe that such constraints naturally correspond to definitions by dependent pattern matching. Motivated by this correspondence, we propose integrating dependent pattern matching into the unification process. We present a prototype implementation of a small dependently typed language that collects delayed unification constraints and resolves them via a pattern matching compiler. Our approach successfully infers solutions that are rejected by current systems such as Rocq and Lean, suggesting a new direction for unification that unifies type inference and pattern matching compilation.
Problem
Pattern-based fragments of higher-order unification used in dependently typed languages cannot synthesize functions defined by case analysis. Such constraints commonly arise from type inference over induction principles, and are rejected by systems like Rocq and Lean.
Approach
The authors observe that these constraints correspond to definitions by dependent pattern matching. They propose extending unification with a second phase: constraints outside the supported pattern fragment are delayed, then reinterpreted as function definitions and passed to a dependent pattern matching compiler for synthesis. A prototype dependently typed language with intrinsically well-scoped syntax, normalization by evaluation, and elaboration-based dynamic unification was implemented in fewer than 3000 lines of Lean.
Results
The prototype successfully infers solutions (such as motives of induction principles) that are rejected by current systems including Rocq and Lean. The approach currently supports inductive families but not recursion or translation of case trees to core terms.
