Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies currently results in puzzling type errors in most of these languages. Yet this combination of features occurs naturally in many scenarios, such as when manipulating typed ASTs. To support it properly, compilers need to implement a form of subtyping reconstruction: the ability to reconstruct subtyping information uncovered at runtime during pattern matching. We introduce cDOT, a new calculus in the family of Dependent Object Types (DOT) intended to serve as a formal foundation for subtyping reconstruction. Being descended from pDOT, itself a formal foundation for Scala, cDOT can be used to encode advanced object-oriented features such as generic inheritance, type constructor variance, F-bounded polymorphism, and first-class recursive modules. We demonstrate that subtyping reconstruction subsumes GADTs by encoding $\lambda_{2,G\mu}$, a classical constraint-based GADT calculus, into cDOT.

翻译：许多面向对象传统的编程语言现已以某种形式支持模式匹配。历史范例包括Scala和Ceylon，以及较新加入的Java、Kotlin、TypeScript和Flow。然而，在这些语言中，对泛型类层次结构的模式匹配通常会导致令人困惑的类型错误。然而，这种特性组合在许多场景中自然出现，例如在操作类型化抽象语法树（AST）时。为了正确支持这一特性，编译器需要实现一种子类型重构的形式：即在模式匹配过程中重构运行时发现的子类型信息的能力。我们引入了cDOT，这是一种属于依赖对象类型（DOT）家族的新演算，旨在作为子类型重构的形式化基础。cDOT继承自pDOT（其本身是Scala的形式化基础），可用于编码高级面向对象特性，例如泛型继承、类型构造器变体、F有界多态性和一等递归模块。我们通过将经典的基于约束的GADT演算$\lambda_{2,G\mu}$编码为cDOT，证明了子类型重构涵盖了GADT。