First-Class Refinement Types
for Scala 3

Refinement types

Outline

We present a work-in-progress implementation of refinement types in Scala 3, with focus on:

• First-class integration: implemented in the Scala compiler directly, not as a plugin or a separate tool.
• Typing: imprecise types by default, recover refinements when needed.
• Runtime checks: pattern matching and sugar.
• Solver: lightweight custom solver for subtyping.
• Mechanization: are we sound yet?

Syntax

Consider the type of non-empty lists:

\{ l: \text{List[A]} \mid l.\text{nonEmpty} \}

type NonEmptyList[A] = { l: List[A] with l.nonEmpty }

Syntax: Shorthand

When a binder already exists, such as in:

def zip[A, B](xs: List[A], ys: {ys: List[B] with ys.size == xs.size})

def zip[A, B](xs: List[A], ys: List[B] with ys.size == xs.size)

Syntax: Example sized List API

def zip[A, B](xs: List[A], ys: List[B] with ys.size == xs.size):
  {l: List[(A, B)] with l.size == xs.size}

def concat[T](xs: List[T], ys: List[T]):
  {res: List[T] with res.size == xs.size + ys.size}

val xs: List[Int] = ...
val ys: List[Int] = ...
zip(concat(xs, ys), concat(ys, xs))
zip(concat(xs, ys), concat(xs, xs)) // error

First-class

Liquid Haskell is a plugin that runs after type checking.

{-@ x :: {v:Int | v mod 2 == 0 } @-}
let x = 42 :: Int in ...

val x: Int with (x % 2 == 0) = 42

First-class: Error messages

Predicates are type-checked like other Scala expressions:

def f[A](l: List[A] with l.notEmpty) = () // error

-- [E008] Not Found Error: tests/neg-custom-args/qualified-types/predicate_error.scala:1:27 ----------------------------
1 |def f[A](l: List[A] with l.notEmpty) = () // error
  |                         ^^^^^^^^^^
  |                         value notEmpty is not a member of List[A]
  |                         - did you mean l.nonEmpty?

First-class: Error messages and inference

Same inference and error reporting as for other Scala types:

def g[T](f: T => Unit, x: T) = f(x)
g((x: PosInt) => x * 2, -2) // error

-- [E007] Type Mismatch Error: tests/neg-custom-args/qualified-types/infer.scala:2:29 ------------------------
2 |  g((x: PosInt) => x * 2, -2) // error
  |                          ^^
  |                          Found:    (-2 : Int)
  |                          Required: {v: Int with v > 0}

First-class: Overload resolution

Consider the following two overloads of min:

/** Minimum of a list. O(n) */
def min(l: List[Int]): Int = l.min

/** Minimum of a sorted list. O(1) */
def min(l: List[Int] with l.isSorted): Int = l.head

val l2: List[Int] with l2.isSorted = l.sorted
min(l2) // calls second overload

Typing

For backward compatibility and performance reasons, refinement types are not inferred from terms by default. The wider type is inferred instead:

val x: /* Int */ = 42

Typing: Selfification

However, when a refinement type is expected, the compiler can selfify the typed expression: that is, to give e: T the refinement type x: T with x == e:

val x: {v: Int with v == 42} = 42

Typing: Local unfolding

The system can also recover precise selfified types from local definitions:

val v1: Int = readInt()
val v2: Int = v1
val v3: Int with (v3 == v1) = v2

Runtime checks

When static checking fails, a refinement type can be checked at runtime using pattern matching:

val idRegex = "^[a-zA-Z_][a-zA-Z0-9_]*$"
type ID = {s: String with s.matches(idRegex)}

"a2e7-e89b" match
    case id: ID =>
        id: ID // matched, id has type ID
    case id     =>
        // default case, did not match

Runtime checks: .runtimeChecked

You can also use .runtimeChecked (SIP-57) when you expect the check to always pass:

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

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

Example: Bound-checked merge sort

Specify a type for non-negative integers (Pos) and a safe division function:

type Pos = {x: Int with x >= 0}

def safeDiv(x: Pos, y: Pos with y > 1): {res: Pos with res < x} =
  (x / y).runtimeChecked

Define an opaque type for bound-checked sequences:

opaque type SafeSeq[T] = Seq[T]

object SafeSeq:
  def fromSeq[T](seq: Seq[T]): SafeSeq[T] = seq
  def apply[T](elems: T*): SafeSeq[T] = fromSeq(elems)

Example: Bound-checked merge sort (2)

Add some methods to SafeSeq:

extension [T](a: SafeSeq[T])
  def len: Pos = a.length.runtimeChecked
  def apply(i: Pos with i < a.len): T =  a(i)
  def ++(that: SafeSeq[T]): SafeSeq[T] = a ++ that
  def splitAt(i: Pos with i < a.len): (SafeSeq[T], SafeSeq[T]) =
    a.splitAt(i)

These methods are only defined for non-empty sequences:

extension [T](a: SafeSeq[T] with a.len > 0)
  def head: T = a.head
  def tail: SafeSeq[T] = a.tail

Example: Bound-checked merge sort (3)

We can match on non-empty sequences, ensuring head and tail are safe to use:

def merge[T: Ordering as ord](left: SafeSeq[T], right: SafeSeq[T]): SafeSeq[T] =
  (left, right) match
    case (l: SafeSeq[T] with l.len > 0, r: SafeSeq[T] with r.len > 0) =>
      if ord.lt(l.head, r.head) then
        SafeSeq(l.head) ++ merge(l.tail, r)
      else
        SafeSeq(r.head) ++ merge(l, r.tail)
    case (l, r) =>
      if l.len == 0 then r else l

Example: Bound-checked merge sort (4)

middle is known to be less than len, so splitAt is safe to use:

def mergeSort[T: Ordering](list: SafeSeq[T]): SafeSeq[T] =
  val len = list.len
  val middle = safeDiv(len, 2)
  if middle == 0 then
    list
  else
    val (left, right) = list.splitAt(middle)
    merge(mergeSort(left), mergeSort(right))

Subtyping

How does the compiler check {x: T with p(x)} <: {y: S with q(y)}?

1. Check T <: S
2. Check p(x) implies q(x) for all x

• constant folding,
• normalization,
• unfolding,
• equality reasoning.

Future work: Flow-sensitive typing

Works with pattern matching:

x match
  case x: Int with x > 0 =>
    x: {v: Int with v > 0}

if x > 0 then
  x: {v: Int with v > 0}

Future work: External checks

Our solver is lightweight 👍 but incomplete 👎.

{v: Int with v > 2} <: {v: Int with v > 0}

x: {v: Int with v > 0} // checked by the type checker
x.runtimeChecked: {v: Int with v > 0} // checked at runtime
x.externallyChecked: {v: Int with v > 0} // checked by an external tool
x.asInstanceOf[{v: Int with v > 0}] // unchecked

Mechanization

Syntax of the language formalized so far:

\begin{aligned} A, B &::= X \mid \texttt{Unit} \mid \texttt{Bool} \mid \Pi x: A.\ B \mid \forall X.\ A \mid \lbrace x : A \mid b \rbrace \mid A \lor B \mid A \land B \\ a, b, f &::= \texttt{unit} \mid \texttt{true} \mid \texttt{false} \mid x \mid \lambda x: A.\ b \mid \Lambda X.\ b \mid f\ a \mid f[A] \\ &\quad \mid \texttt{let}\ x : A = b\ \texttt{in}\ a \mid a == b \mid \texttt{if}\ a\ \texttt{then}\ b_1\ \texttt{else}\ b_2 \end{aligned}

Mechanization: Interpretation

A semantic type is a predicate on values. The interpretation ⟦ A ⟧_{\delta}^{\rho} maps a syntactic type A to a semantic type, given a type variable environment \delta and a value environment \rho:

\begin{aligned} \cdots\\ ⟦ \texttt{Bool} ⟧_{\delta}^{\rho} &= \lambda v.\ v = \texttt{true} \lor v = \texttt{false} \\ \cdots\\ ⟦ \lbrace x : A \mid p \rbrace ⟧_{\delta}^{\rho} &= \lambda v.\ ⟦ A ⟧_{\delta}^{\rho}(v) \land \rho, x \mapsto v \vdash p \Downarrow \texttt{true} \\ \cdots\\ \end{aligned}

Mechanization: Typing

The rule for let-bindings that stores equalities in the fact context:

\frac{\Gamma \vDash a : A \qquad \text{firstorder}(A) \qquad \Gamma, x : A, \lbrace x == a \rbrace \vDash b : B}{\Gamma \vDash \texttt{let}\ x : A = a\ \texttt{in}\ b : \text{avoid}(B, x)} \text{(T-LetEq)}

The rule for selfification:

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

The rule for if expressions:

\frac{\Gamma \vDash a : \texttt{Bool} \qquad \Gamma, \lbrace a == \texttt{true} \rbrace \vDash b_1 : B_1 \qquad \Gamma, \lbrace a == \texttt{false} \rbrace \vDash b_2 : B_2}{\Gamma \vDash \texttt{if}\ a\ \texttt{then}\ b_1\ \texttt{else}\ b_2 : B_1 \lor B_2} \text{(T-If)}

Conclusion

• Syntax: {x: T with p(x)}, can omit binder,
• First-class: integrates with Scala UX and features (overloading, extension methods, givens, etc.),
• Typing: imprecise types by default, can recover refinements using selfification and local unfolding,
• Runtime checks: pattern matching, .runtimeChecked,
• Subtyping: normalization, local unfolding, equality reasoning, compatibility with other types,
• Future work: flow-sensitive typing, external checks,
• Mechanization: System F with refinement types and more, using a definitional interpreter and semantic types.

Backup: Predicate restrictions

var x = 3
val y: Int with y == 3 = x // ⛔️ x is mutable

class Box(val value: Int)
val b: Box with b == Box(3) = Box(3) // ⛔️ Box has equality by reference

Backup: LH Usability Barriers

From “Usability Barriers for Liquid Types” [1]:

• 4.2 Unclear Divide between Haskell and LiquidHaskell:
  • “comments are usually seen as just optional information in the code and not something that is directly used by the compiler”
  • “It’s sort of like you’re doing two things at once because you’re implementing in Haskell. But you’re also talking to GHC, but you’re also talking to LiquidHaskell.”
• 4.7 Unhelpful Error Messages
  • “[…] error messages produced from typing errors inside the predicates, seemed indistinguishable from those produced by verification errors.”
• 4.8 Limited IDE Support
  • “[user] tried to use the function length, but since it was not imported, it was impossible to use in this case.”

[1] Catarina Gamboa, Abigail Reese, Alcides Fonseca, and Jonathan Aldrich. 2025. Usability Barriers for Liquid Types. Proc. ACM Program. Lang. 9, PLDI, Article 224 (June 2025), 26 pages. doi:10.1145/3729327

Backup: List.collect

Scala type parameters are erased at runtime, so we cannot match on a List[T].

type Pos = { v: Int with v >= 0 }

val xs = List(-1,2,-2,1)
xs.collect { case x: Pos => x } : List[Pos]

Backup: Specify using assertions 😕

def zip[A, B](
  xs: List[A],
  ys: List[B]
) : List[(A, B)] = {
  require(xs.size == ys.size)
  ...
}.ensuring(_.size == xs.size)

Backup: Specify using dependent types 😕

def zip[A, B](
  xs: List[A],
  ys: List[B] {
    val size: xs.size.type
  }
): List[(A, B)] {
  val size: xs.size.type
} = ...

Future work: term-parameterized types

extension [T](list: List[T])
  def get(index: Int with index >= 0 && index < list.size): T = ...

type Range(from: Int, to: Int) = {v: Int with v >= from && v < to}
extension [T](list: List[T])
  def get(index: Range(0, list.size)): T = ...

Future work: Flow-sensitive typing (2)

This would be required for reasoning with refinement types inside cases:

enum MyList[+T]:
  case Cons(head: T, tail: MyList[T])
  case Nil

def myLength(xs: MyList[Int]): Int =
  xs match
    case MyList.Nil =>
      // Add assumption xs == MyList.Nil
      0
    case MyList.Cons(_, xs1) =>
      // Add assumption xs == MyList.Cons(?, xs1)
      1 + myLength(xs1)

Subtyping: Constant folding

{v: Int with v == 1 + 1}     <: {v: Int with v == 2}

Subtyping: Normalization

Arithmetic expressions are normalized using standard algebraic properties, for example commutativity of addition:

{v: Int with v == x + 1}     <: {v: Int with v == 1 + x}

{v: Int with v == y + x}     <: {v: Int with v == x + y}

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

Subtyping: Local unfolding

As mentioned, refinement types are not inferred from terms by default. However, the solver can unfold definitions of local val (only), even when they have an imprecise type:

val x: Int = ...
val y: Int = x + 1

{v: Int with v == y} =:= {v: Int with v == x + 1}

Subtyping: Equality reasoning

Transitivity of equality:

{v: Int with v == a && a == b} <: {v: Int with v == b}

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

Subtyping: With other Scala types

Literal types are subtypes of singleton refinement types:

3 <: {v: Int with v == 3}