扩展摘要：从模式统一到模式匹配统一
Extended Abstract: From Pattern Unification Towards Pattern Matching Unification
AI总结：
研究高阶统一在依赖类型语言中的作用，发现现有模式片段局限。受约束与依赖模式匹配对应关系启发，将其集成到统一过程，通过原型实现展示能推断当前系统拒绝的解决方案，为统一提供新方向。
AI中文摘要：
我们重新审视高阶统一在依赖类型语言中的作用，并确定了现有基于模式的片段的一个基本限制：它们无法合成通过案例分析定义的函数。即使是类型推断产生的简单且普遍的约束，特别是归纳原理的使用，也超出了米勒模式及其现代扩展的表达能力。我们发现此类约束自然对应于依赖模式匹配的定义。受此对应关系的启发，我们提议将依赖模式匹配集成到统一过程中。我们展示了一种小型依赖类型语言的原型实现，该语言收集延迟的统一约束并通过模式匹配编译器解决它们。我们的方法成功推断出当前系统（如 Rocq 和 Lean）拒绝的解决方案，为统一类型推断和模式匹配编译的统一提供了新方向。
英文摘要：
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.
