Scala Type-Level Programming, in depth: literal types, match types, compiletime ops, inline and given-driven proofs

Types as values: singletons and literals

To compute with types you need types that carry information. Scala 3 gives every literal its own type: the type 3 has exactly one inhabitant, the value 3, and is a subtype of Int. The same holds for strings, booleans and other literals, and x.type is the singleton type of any stable value. Once the number 3 can appear in a type position, a type parameter such as N <: Int can stand for a specific number, and the compiler can check relationships between numbers the way it checks relationships between classes.

Two bridges connect the two worlds. Going from type to value, ValueOf[N] is a given the compiler synthesises for any singleton type, and scala.compiletime.constValue[N] does the same inside inline code. Going from value to type happens through inference: write val n: 3 = 3 or pass a literal where a singleton is expected and the narrow type is kept.

val three: 3 = 3                       // literal type
def show[N <: Int](using v: ValueOf[N]): String = s"N = ${v.value}"
show[42]                               // "N = 42"; the given is synthesised from the type

The three engines

Scala 3 has three mechanisms that run during type checking, and type-level code is a combination of them. Match types compute a type from a type, like a function whose cases are patterns on types. Given search, the successor to implicits, proves that a type has some property by finding or building an instance; it behaves like a small logic-programming engine, which is how Scala 2 libraries did all their type-level work. Inlining expands an inline def at the call site and can branch on types and constants while doing so, so the code that survives depends on what the compiler knew.

The diagram also shows the most important practical fact. Type information is erased before code generation, so a type-level guarantee costs nothing at run time, but anything you want to use at run time, such as the actual length 3, has to be carried across deliberately with ValueOf, constValue or an inlined branch.

Match types: functions from types to types

A match type is defined like a pattern match over a type parameter. The standard example from the Scala 3 reference maps a container type to its element type:

type Elem[X] = X match
  case String      => Char
  case Array[t]    => t
  case Iterable[t] => t

val c: Elem[String]       = 'a'      // Char
val i: Elem[List[Int]]    = 1        // Int

Match types may be recursive, and a method whose result type is a match type can be implemented with an ordinary value-level match whose cases mirror the type cases; the compiler checks the two line up:

type LeafElem[X] = X match
  case String      => Char
  case Array[t]    => LeafElem[t]
  case Iterable[t] => LeafElem[t]
  case AnyVal      => X

def leafElem[X](x: X): LeafElem[X] = x match
  case x: String      => x.charAt(0)
  case x: Array[t]    => leafElem(x(0))
  case x: Iterable[t] => leafElem(x.head)
  case x: AnyVal      => x

Reduction has one rule that surprises everyone. The compiler tries cases in order, and it may only skip a case if it can prove the scrutinee is disjoint from that case's pattern. For final classes and literal types that proof is easy. For an abstract type parameter or a non-sealed trait it is not, so the match type stays unreduced, or stuck, and you see a type such as Elem[T] in an error where you expected Int. Stuck types are the most common failure in type-level Scala 3. The fix is usually to reduce later, at a call site where the type is concrete, or to make the types involved final or sealed.

Tuples are where match types earn their keep in everyday code. A Scala 3 tuple is a type-level list built from *: and EmptyTuple, and the standard library provides match types over it, including Tuple.Map, Tuple.Concat and Tuple.Size:

type Row      = (Int, String, Double)
type Nullable = Tuple.Map[Row, Option]       // (Option[Int], Option[String], Option[Double])
type Wide     = Tuple.Concat[Row, (Boolean, Long)]

type Last[T <: Tuple] = T match
  case x *: EmptyTuple => x
  case _ *: tail       => Last[tail]
val d: Last[Row] = 2.5                        // Double

Compile-time arithmetic with scala.compiletime.ops

Literal types become useful for sizes and indices once you can do arithmetic on them. The package scala.compiletime.ops defines type-level operators for Int, Long, Boolean and String. They reduce when their arguments are literal types and stay symbolic otherwise, which is exactly what lets a method say its result has length N + M without knowing either number:

import scala.compiletime.ops.int.*

val five: 2 + 3 = 5
val yes: 3 < 4  = true
type Half[N <: Int] = N / 2
val h: Half[10] = 5

Inline code reaches the same information from the term side. constValue[N] turns a literal type into a value, erasedValue[T] lets an inline match branch on a type without a value, and error stops compilation with your own message when a branch is selected:

import scala.compiletime.{constValue, erasedValue, error, codeOf}

inline def port(inline p: Int): Int =
  inline if p >= 1 && p <= 65535 then p
  else error("port out of range: " + codeOf(p))

inline def defaultOf[T]: T = inline erasedValue[T] match
  case _: Int     => 0.asInstanceOf[T]
  case _: String  => "".asInstanceOf[T]
  case _: Boolean => false.asInstanceOf[T]

val ok  = port(8080)
// val bad = port(70000)   // compile error: port out of range: 70000

Worked example: vectors that know their length

Consider a feature pipeline that combines fixed-width embedding vectors. Adding a 384-wide vector to a 768-wide one is a bug that normally surfaces as a runtime exception, or worse as silent truncation by a zip. Encoding the width in the type makes it a compile error. The class below keeps its constructor private so the only ways in are checked: a fill whose length comes from the type, and a validating conversion from untyped data at the boundary.

import scala.compiletime.ops.int.*

final class Vec[N <: Int] private (val data: Vector[Double]):
  def +(that: Vec[N]): Vec[N]   = new Vec[N](data.lazyZip(that.data).map(_ + _))
  def dot(that: Vec[N]): Double = data.lazyZip(that.data).map(_ * _).sum
  def ++[M <: Int](that: Vec[M]): Vec[N + M] = new Vec[N + M](data ++ that.data)

object Vec:
  def fill[N <: Int](x: Double)(using n: ValueOf[N]): Vec[N] =
    new Vec[N](Vector.fill(n.value)(x))

  def from[N <: Int](xs: Vector[Double])(using n: ValueOf[N]): Either[String, Vec[N]] =
    if xs.size == n.value then Right(new Vec[N](xs))
    else Left(s"expected ${n.value} values, got ${xs.size}")

val a = Vec.fill[3](1.0)
val b = Vec.fill[2](2.0)
val joined: Vec[5] = a ++ b        // 3 + 2 reduces to 5
val sum = a + a                    // fine
// a + b                           // error: Found Vec[2], Required Vec[3]
val parsed = Vec.from[768](rowFromParquet)   // Either: validated once at the edge

Walk through what the compiler does with a ++ b. It infers N = 3 from a and M = 2 from b, so the result type is Vec[3 + 2]; because both arguments are literals, the ops package reduces that to Vec[5] and the ascription checks. In a generic method where N is still abstract, the result stays Vec[N + M], which is correct but means callers see symbolic types until they become concrete. After erasure, Vec is a plain wrapper around Vector[Double]: the proof cost nothing at run time.

The from method is the pattern to copy. Type-level guarantees only hold for values created through checked paths, so validate once where untyped data enters, such as a file, a request or a database row, and let the types carry the guarantee from there. The same idea, applied to a single value instead of a size, is what opaque types give you.

Typestate: making illegal sequences unrepresentable

Type parameters that carry no data, called phantom types, can encode a protocol. Here a connection must be opened before it is queried and cannot be closed twice. The methods are only available when the state parameter has the right type, using a using clause that demands evidence of type equality:

sealed trait State
final class Closed extends State
final class Open   extends State

final class Conn[S <: State] private (url: String):
  def open(using S =:= Closed): Conn[Open]          = new Conn[Open](url)
  def query(sql: String)(using S =:= Open): List[String] = List(s"rows for $sql")
  def close(using S =:= Open): Conn[Closed]         = new Conn[Closed](url)

object Conn:
  def apply(url: String): Conn[Closed] = new Conn[Closed](url)

val c1 = Conn("jdbc:postgresql://db/app").open
c1.query("select 1")
val c2 = c1.close
// c2.query("select 1")   // error: Cannot prove that Closed =:= Open

The =:= evidence only needs the states to be distinct types: the compiler synthesises A =:= A and nothing else. Declaring the markers as final classes adds something for later: it makes them provably disjoint, so match types written over the state reduce instead of getting stuck. The markers are never instantiated; they exist only as types.

The Scala 2 way: Aux and implicit induction

Before match types, all type-level computation ran through implicit search, and much of the ecosystem, including shapeless 2, still looks like this. A type class with an abstract output type member acts as a function, and implicit definitions act as its recursive cases. The Aux alias exposes the output as a type parameter so it can be chained:

sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat

trait Sum[A <: Nat, B <: Nat] { type Out <: Nat }
object Sum {
  type Aux[A <: Nat, B <: Nat, O <: Nat] = Sum[A, B] { type Out = O }
  implicit def zero[B <: Nat]: Aux[_0, B, B] = new Sum[_0, B] { type Out = B }
  implicit def succ[A <: Nat, B <: Nat](implicit s: Sum[A, B]): Aux[Succ[A], B, Succ[s.Out]] =
    new Sum[Succ[A], B] { type Out = Succ[s.Out] }
}

This works, but every step costs an implicit search, unary numbers grow linearly, and a failed proof reports only that an implicit was not found. In Scala 3, prefer match types and compiletime ops for computation and reserve givens for proofs and type-class derivation. How the compiler resolves those givens is covered in implicit resolution, and the generic-derivation style built on this pattern in the shapeless article.

Costs, limits and failure modes

There is also a social cost. Every type-level trick is something the next maintainer must learn. Use it where a mistake is expensive and frequent, such as dimensions, units, protocol states and schema mappings, and keep the advanced machinery behind a small, ordinary-looking API. When you need to generate code rather than check it, move up to Scala 3 macros.

What to do next

1. Pick one recurring runtime bug in your codebase, such as a dimension mismatch or a call in the wrong state, and write down the invariant it violates.
2. Encode it with the simplest tool that works: a literal type and ValueOf, a phantom state parameter, or an opaque type.
3. Hide the constructor and add a single validating entry point for untyped input.
4. Write a compile-failure test for the bad case, for example with scala.compiletime.testing.typeCheckErrors, so the guarantee cannot silently regress.
5. Reach for match types only when you need to compute a type; keep cases disjoint and test them with concrete ascriptions.
6. Measure compile time before and after, and roll back any trick that costs more build time than the bugs it prevents.