Short form, reusing a name already in scope:

val x: (Int with x % 2 == 0) = 42
// desugars to:
val x: {v: Int with v % 2 == 0} = 42

“It’s sort of like you’re doing two things at once […] you’re also talking to GHC, but you’re also talking to LiquidHaskell.” – Usability Barriers for Liquid Types (Gamboa et al., PLDI 2025)

Instead, we implement refinement as ordinary Scala types, participating in subtyping, inference, overloading and pattern matching.

// Example: Bounded polymorphism
type Even = {v: Int with v % 2 == 0}
def maximum[T: Ordering, U <: T]
  (xs: List[U]): U = xs.reduce(max)
def example1: Even =
  maximum(List(2, 4, 6))

// Example: Overload resolution
def min(l: List[Int] with l.isSorted) =
  l.head // O(1)
def min(l: List[Int]) = l.min // O(n)

def ex2(l: List[Int] with l.isSorted) =
  min(l) // calls the first overload

Why not always infer the precise type?

1. Backward compatibility: implicit and overload resolution depend on inferred types; a more precise type changes which instances are found.
2. Performance: bigger types, slower comparisons.
3. Usability: inferring most precise types everywhere would be unreadable.

Instead, precision is recovered on demand, by a standard mechanism called selfification, triggered by the bidirectional type-inference algorithm:

val x: (Int with x == 42) = 42 // selfified

Checked casts. .runtimeChecked (SIP-57), when you expect the check to pass:

val id: ID = "a2e7-e89b".runtimeChecked

// desugars to:
val id: ID =
  if ("a2e7-e89b".matches(idRegex))
    "a2e7-e89b".asInstanceOf[ID]
  else throw new IllegalArgumentException()

Existing implementations lower to SMT.

Due to packaging and performance concerns, we instead implemented our own lightweight e-graph-based solver.

{v: Int with v == a && a == b}
  <: {v: Int with v == b}
{v: Int with a == b}
  <: {v: Int with f(a) == f(b)}

And domain-specific normalizations such as:

{v: Int with v == x + 3 * y}
  <: {v: Int with v == 2 * y + (x + y)}

Also beta-reduction, ADT constructors and limited reasoning for linear integer arithmetic.

When the feature is unused, the full Dotty CI passes unchanged: the compiler itself (≈200 000 LoC),
≈10 000 tests, a 50-project community build.

≤ 4% slowdown on the official benchmark suite.

Expressiveness. Because refinements are types, we get type-argument inference. We also compile unmodified Scala, so adoption is incremental.

Conversely, both alternatives have stronger solvers: SMT-backed and complete for linear integer arithmetic, ADTs and equality.

Loops. \textsf{loop}(a)\; x.\, b is a limited recursion that suffices to model loops and tail recursion. The body returns \textsf{inl} to continue, \textsf{inr} to exit.

Contribution. To our knowledge, this is the first mechanized soundness proof combining refinements with \lor/\land, bounded polymorphism (both bounds), and positive equi-recursive types.

\mathcal{V}\llbracket A \rrbracket_{\delta}^{\rho} is a predicate Value -> Prop, also known as a semantic type.

The term interpretation \mathcal{E}\llbracket A \rrbracket_{\delta}^{\rho}(t) lifts it to terms:

\begin{aligned} \mathcal{E}\llbracket A \rrbracket_{\delta}^{\rho}(a) \triangleq\ & \forall n, r.\; \texttt{eval}\; n\; \rho\; a = \texttt{Some}\; r \implies \\ &\quad \exists v.\; r = \texttt{Some}\; v \land \mathcal{V}\llbracket A \rrbracket_{\delta}^{\rho}(v) \end{aligned}

“If evaluation terminates, it produces a value (not stuck), and that value is in \mathcal{V}\llbracket A \rrbracket.” Vacuously true for diverging terms; this is partial correctness.

Value interpretation of function types:

\begin{aligned} \mathcal{V}\llbracket \Pi x{:}A.\, B \rrbracket_{\delta}^{\rho}(v) \triangleq\ & \exists \rho_f, b.\; v = \langle \rho_f, \lambda x.\, b \rangle\ \land \\ & \forall v_a.\; \mathcal{V}\llbracket A \rrbracket_{\delta}^{\rho}(v_a) \implies \mathcal{E}\llbracket B \rrbracket_{\delta}^{\rho_f[x \mapsto v_a]}(b) \end{aligned}

Value interpretation of refinement types:

\mathcal{V}\llbracket \lbrace x : A \mid p \rbrace \rrbracket_{\delta}^{\rho}(v) \triangleq \mathcal{V}\llbracket A \rrbracket_{\delta}^{\rho}(v) \land \mathcal{E}\llbracket \texttt{True} \rrbracket_{\delta}^{\rho[x \mapsto v]}(p)

Value interpretation of recursive types:

\mathcal{V}\llbracket \mu X.\, A \rrbracket_{\delta}^{\rho}(v) \triangleq \forall n.\; F^n(v)

F^0(v) = \top,\quad F^{n+1}(v) = \mathcal{V}\llbracket A \rrbracket_{\delta[X \mapsto F^n]}^{\rho}(v)

A context \Gamma is made of:

1. Term bindings: x : A
2. Type variable bindings: X >: A <: B
3. Equality facts: s \sim t

The usual typing rules are not definitions but lemmas: each rule is proven individually.

Rule for let-bindings:

\frac{\Gamma \vDash a : A \qquad \Gamma, x : A, x \sim a \vDash b : B}{\Gamma \vDash \textsf{let}\; x{:}A = a \;\textsf{in}\; b : \textsf{avoid}(B, x)}\;\text{(T-Let)}

Selfification rule:

\frac{\Gamma \vDash a : A \qquad \textsf{firstorder}(A)}{\Gamma \vDash a : \lbrace x : A \mid x \mathbin{\texttt{==}} a \rbrace}\;\text{(T-Self)}

Every value satisfying A also satisfies B.

Recursive types are equi-recursive:

\frac{\textsf{spos}(X, A)}{\Gamma \vDash \mu X.\, A <: A[X \mapsto \mu X.\, A]}\;\text{(S-Mu-Unfold)}

\frac{\textsf{spos}(X, A)}{\Gamma \vDash A[X \mapsto \mu X.\, A] <: \mu X.\, A}\;\text{(S-Mu-Fold)}

Together they give \mu X.\, A <:> A[X \mapsto \mu X.\, A], provided X occurs only strictly positively in A: never left of an arrow, nor in a \forall bound.

Subtyping between refinements is semantic implication, a.k.a. entailment:

\frac{\Gamma \vDash A <: B \qquad \Gamma, x : A \vDash p_1 \Rightarrow p_2}{\Gamma \vDash \lbrace x : A \mid p_1 \rbrace <: \lbrace x : B \mid p_2 \rbrace}\;\text{(S-Refine)}

A refinement \lbrace x : A \mid p \rbrace holds when p evaluates to true whenever it terminates. Implication reads both predicates that way:

\begin{aligned} \Gamma \vDash p_1 \Rightarrow p_2 \triangleq\ & \forall \delta, \rho.\; \mathrm{wf}(\delta, \Gamma, \rho) \implies \\ &\quad \mathcal{E}\llbracket \texttt{True} \rrbracket(p_1) \implies \mathcal{E}\llbracket \texttt{True} \rrbracket(p_2) \end{aligned}

Lemma:

\Gamma \vDash \lbrace x : A \mid \textsf{diverge} \rbrace \mathrel{<:>} \lbrace x : A \mid \texttt{true} \rbrace \mathrel{<:>} A