First-Class Refinement Types for Scala

TL;DR

This paper introduces first-class refinement types for Scala 3, enabling integrated, expressive, and type-safe logical predicates within the language's type system.

Contribution

It designs and proves soundness for a core calculus of first-class refinements, and implements a prototype extension of Scala 3 with a solver for predicate entailment.

Findings

Type soundness of the core calculus is proven.

Refinements participate in subtyping, inference, and pattern matching.

Prototype implementation demonstrates practical integration in Scala 3.

Abstract

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.