Refinement types -- types qualified with logical predicates -- have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate specification language or treated as second-class annotations, disconnected from the host language's type system. This disconnect creates usability barriers: programmers must maintain two mental models, and refinements cannot interact with features like type inference, subtyping, or overloading. We present the design of first-class refinement types for Scala 3, where refinements are ordinary types that participate in subtyping, inference, and pattern matching alongside existing language features. We prove type soundness of a core calculus mechanized in Rocq, combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types under a partial-correctness semantics using a fuel-bounded definitional interpreter and semantic typing. Finally, we implement our design as a prototype extension of the Scala 3 compiler with a lightweight e-graph-based solver for predicate entailment.

翻译：精炼类型——以逻辑谓词限定的类型——已在Liquid Haskell、F*和Dafny等语言中证明对于轻量级验证有效。然而，在这些系统中，精炼要么以单独规范语言编写，要么被视为二等注解，与宿主语言的类型系统脱节。这种脱节造成了可用性障碍：程序员必须维护两种心智模型，且精炼无法与类型推断、子类型或重载等功能交互。我们提出Scala 3一等精炼类型的设计，其中精炼是参与子类型、推断和模式匹配的普通类型，与现有语言特性协同工作。我们通过Rocq机械化核心演算的类型安全性证明，结合依赖函数类型、有界多态、正互递归类型、并集与交集类型，以及在部分正确性语义下使用基于燃料的定义解释器和语义类型的精炼类型。最后，我们的设计实现为Scala 3编译器的原型扩展，采用基于轻量级e-图的求解器处理谓词蕴含。