Scala 3's Type System, Part 10: GADTs, Variance, and the Frontier

scalatype-systems

Two questions close out this series. Why is List[Dog] a List[Animal] while Array[Dog] is emphatically not an Array[Animal], and why does a single eval function get to return Int for one case and Boolean for another without a cast? The answers are variance and GADTs, and both are things you want to be able to predict rather than look up.

🔗The problem: a container that lies

Java made covariant arrays a language rule. This compiles:

Object[] arr = new String[1];
arr[0] = Integer.valueOf(42);   // ArrayStoreException at runtime

Every Java array store carries a runtime type check to catch that, and the failure is an ArrayStoreException thrown from an assignment that the compiler approved. Scala refuses the program instead, because Array is invariant:

// scala-check: expect-error
class Animal
class Dog extends Animal
class Cat extends Animal

@main def demo(): Unit =
  val dogs: Array[Dog] = Array(new Dog)
  val animals: Array[Animal] = dogs      // rejected here
  animals(0) = new Cat
-- [E007] Type Mismatch Error --------------------------------------------
8 |  val animals: Array[Animal] = dogs
  |                               ^^^^
  |                               Found:    (dogs : Array[Dog])
  |                               Required: Array[Animal]

The rule underneath: a container you can only read from may be covariant; a container you can also write to may not.

🔗Covariance, contravariance, and predicting the error

Mark a type parameter +A and F[Dog] <: F[Animal]. Mark it -A and the subtyping flips: F[Animal] <: F[Dog]. Producers are covariant, consumers are contravariant.

class Animal
class Dog extends Animal

final class Box[+A](val value: A)          // produces A
trait Sink[-A]:                            // consumes A
  def send(a: A): Unit

@main def demo(): Unit =
  val animalBox: Box[Animal] = Box(new Dog)          // covariance
  val anySink: Sink[Animal] = a => println(a)
  val dogSink: Sink[Dog] = anySink                   // contravariance
  dogSink.send(new Dog)

Sink[Dog] = anySink reads oddly until you say it out loud: something that accepts any animal is a perfectly good place to send dogs.

Function types combine both — Function1[-T, +R] — which is why this is legal:

class Animal
class Dog extends Animal

val f: Dog => String = (a: Animal) => a.toString

A function that handles all animals can stand in wherever one that handles dogs is expected, and its return type can be more specific.

Now the rule that lets you predict the compiler’s complaint. Every occurrence of a type parameter sits in a position, and positions flip:

Where A appearsPosition
Method result type, val typecovariant
Method parameter typecontravariant
Inside a +X type argumentkeeps the surrounding position
Inside a -X type argumentflips the surrounding position
Inside an invariant type argumentinvariant — nothing is allowed
var field typeinvariant

A +A may appear only in covariant positions, a -A only in contravariant ones. Flips compose, which is why this whole trait is fine despite A sitting inside function parameters:

trait Source[+A]:
  def head: A                             // covariant: fine
  def foreach(f: A => Unit): Unit         // param of a param: flipped twice
  def fold[B](z: B)(op: (B, A) => B): B   // same, fine

And why this one is not:

// scala-check: expect-error
import scala.collection.mutable.ListBuffer

trait Source[+A]:
  def collectInto(buffer: ListBuffer[A]): Unit
covariant type A occurs in invariant position in type ListBuffer[A]
of parameter buffer

ListBuffer is invariant, so once A is under it, no amount of position flipping helps.

🔗The lower-bound fix

The canonical failure is a covariant collection with an “add” method:

// scala-check: expect-error
final class Stack[+A](items: List[A]):
  def push(a: A): Stack[A] = Stack(a :: items)
covariant type A occurs in contravariant position in type A
of parameter a

The fix is not to drop the +. It is to accept a wider element and return a wider stack — exactly what List.:: and List.:+ do:

final class Stack[+A](private val items: List[A]):
  def push[B >: A](b: B): Stack[B] = Stack(b :: items)
  def top: Option[A] = items.headOption

class Animal
class Dog extends Animal
class Cat extends Animal

@main def demo(): Unit =
  val dogs: Stack[Dog] = Stack(List(new Dog))
  val animals: Stack[Animal] = dogs.push(new Cat)   // widens to the LUB
  println(animals.top)

B is a fresh parameter, so it occupies a contravariant position legally, and the result type honestly reports that you now have a stack of something more general. Pushing a Cat onto a Stack[Dog] gives you a Stack[Animal] rather than a lie.

The standard library is not uniformly variant. Ordering[T] is a pure consumer and yet is invariantOrdering[Animal] will not be accepted where Ordering[Dog] is wanted. That is a historical artifact of its Comparator/PartialOrdering ancestry, not a principle. Check before you assume.

🔗GADTs: an evaluator that type-checks

Here is the motivating case. A small expression language where the type parameter records what each expression evaluates to:

enum Expr[A]:
  case Lit(i: Int) extends Expr[Int]
  case Bool(b: Boolean) extends Expr[Boolean]
  case Add(l: Expr[Int], r: Expr[Int]) extends Expr[Int]
  case Eq[B](l: Expr[B], r: Expr[B]) extends Expr[Boolean]
  case If[A](c: Expr[Boolean], t: Expr[A], e: Expr[A]) extends Expr[A]

import Expr.*

def eval[A](e: Expr[A]): A = e match
  case Lit(i)      => i
  case Bool(b)     => b
  case Add(l, r)   => eval(l) + eval(r)
  case Eq(l, r)    => eval(l) == eval(r)
  case If(c, t, f) => if eval(c) then eval(t) else eval(f)

@main def demo(): Unit =
  println(eval(If(Eq(Lit(1), Lit(1)), Add(Lit(2), Lit(3)), Lit(0))))

Look at the first branch. The declared result type is A, and the branch returns an Int. That is only sound because of what the match taught the compiler: Lit extends Expr[Int], so if this value is a Lit and its static type is Expr[A], then A must be Int in this branch and nowhere else.

That is the whole idea of GADT reasoning: matching a case introduces a local type equality about the type parameter. The compiler records A =:= Int for the duration of that branch, uses it to accept i, and discards it at the next case. In the Bool branch it has A =:= Boolean instead. There is no runtime tag inspection and no cast — the constructor already carried the evidence.

Scala 2 could declare that same Expr, but its inference could not exploit the equality, so the standard workaround was to cast:

// scala-check: skip
// Scala 2 — the shape everyone wrote
def eval[A](e: Expr[A]): A = (e match {
  case Lit(i)  => i
  case Bool(b) => b
}).asInstanceOf[A]

That works and is unsatisfying: the cast is doing no work at runtime, it exists only to silence the compiler, and it silences genuinely wrong branches too. Scala 3 removes the need.

🔗Where GADT inference still gives up

Two limits are worth knowing, because both produce errors that look like the compiler being obtuse.

Omitting the result type disables the payoff. GADT constraints refine each branch, but with no declared result type the branches are joined into a union:

// scala-check: expect-error
enum Expr[A]:
  case Lit(i: Int) extends Expr[Int]
  case Bool(b: Boolean) extends Expr[Boolean]

import Expr.*

def eval[A](e: Expr[A]) = e match   // no `: A`
  case Lit(i)  => i
  case Bool(b) => b

@main def demo(): Unit =
  val n: Int = eval(Lit(1))         // Found: Int | Boolean

Always annotate the result type of a GADT match. This is not a style preference; it is what turns the constraint on.

Type members do not get GADT refinement — only type parameters do. If you model the same evaluator with the path-dependent style from Part 9, it does not work:

// scala-check: expect-error
trait Expr:
  type Value

case class Lit(i: Int) extends Expr:
  type Value = Int

case class Bl(b: Boolean) extends Expr:
  type Value = Boolean

def eval(e: Expr): e.Value = e match
  case Lit(i) => i     // Found: (i : Int)  Required: e.Value
  case Bl(b)  => b

Matching on Lit tells the compiler the value e is a Lit, but it does not propagate that into the abstract type projection e.Value. The workaround is mechanical and slightly annoying: convert the type member into a type parameter (trait Expr[A]) and the enum-style code above starts working. If you need the type-member formulation for other reasons, you are back to a cast.

Beyond these, GADT constraint solving gets weaker as the relationship between the case’s parent type and the scrutinee’s type gets more indirect — nesting under abstract type constructors, or type parameters that occur in multiple positions. When it fails, the message is a plain type mismatch with no hint that a constraint was expected, which is the frustrating part.

🔗The frontier

Everything in this section is experimental. It requires nightly builds, -experimental, or a specific import language.experimental.*, and the syntax has already changed at least once for most of these. Do not build a production codebase on any of it. All snippets below are illustrative only.

Safer exceptions turns checked exceptions into an implicit capability. A throws clause introduces a required CanThrow[E], and try/catch provides one:

// scala-check: skip
import language.experimental.saferExceptions

class InsufficientFunds extends Exception

def withdraw(balance: Long, amount: Long): Long throws InsufficientFunds =
  if amount > balance then throw InsufficientFunds() else balance - amount

@main def demo(): Unit =
  try println(withdraw(100, 500))
  catch case _: InsufficientFunds => println("declined")

Calling withdraw outside a catch for that exception is a compile error. Java’s checked exceptions with the ergonomics fixed, essentially, though the interaction with higher-order functions is where the hard parts live.

Capture checking is the ambitious one: tracking which capabilities a value holds, so the compiler can tell you a resource escaped the scope that owns it. The ^ suffix marks a type as capturing something:

// scala-check: skip
import language.experimental.captureChecking

// `logger` is valid only inside `op`; the ^ says the type captures a capability
def withLogger[T](path: String)(op: Logger^ => T): T = ???

// Rejected: the logger escapes, and would be used after close.
val leaked = withLogger("app.log")(logger => logger)

If this lands, use-after-close and leaked Iterators over closed streams become compile errors, and effect tracking gets a foundation that does not require wrapping everything in a monad. It is also the largest change to Scala’s typing rules since 3.0 and is still moving.

Named tuples give tuples labeled fields, so a query result or a small record needs no case class:

// scala-check: skip
type Order = (id: String, total: Long)

val o: Order = (id = "A-1", total = 1250L)
val cheap = o.total < 500

This one has progressed furthest — it graduated out of the experimental import in 3.7 — but treat the surrounding tooling and library support as young.

into and the conversion rework narrows implicit conversions from a global hazard to an opt-in at a specific parameter. The callee declares where a conversion may fire; nowhere else:

// scala-check: skip
import language.experimental.into

case class Route(segments: List[String])
given Conversion[String, Route] = s => Route(s.split("/").toList)

def handle(r: into Route): String = r.segments.mkString("/")

handle("orders/1")   // conversion allowed here, and only here

The spelling of into has already changed once between releases. The direction — conversions become a property of the API rather than of the import scope — is the part to remember.

🔗Retrospective: ten parts

The arc was the three jobs from Part 1.

Model data so illegal states cannot be built. Enums and ADTs, union and intersection types, and opaque types. This is the part with an immediate payoff and essentially no cost. Every application codebase should be using all three.

Abstract over behavior. Given/using and type classes and derivation pay off around the third caller. Higher-kinded types and type lambdas are mostly a library concern — reach for them when you are writing the abstraction, not when you are consuming one.

Compute at compile time. Match types, dependent and structural types, and GADTs. These are where compile times go and where error messages get long. They earn their place in a library that thousands of call sites depend on, and rarely in application code.

If I had to compress the practical advice into one table:

FeatureApplication codeLibrary code
Enums / ADTsYes, everywhereYes
Opaque typesYes, for identifiers and unitsYes
Union typesYes, for error channelsSparingly
Type classes (given/using)Yes, once you have three callersCore tool
DerivationConsume itWrite it
Higher-kinded typesRarelyYes
Match typesNoYes, with care
Literal / dependent typesFor a typed config, maybeYes
Structural typesOnly at dynamic edgesAt dynamic edges
GADTsIf you have an interpreterYes
Variance annotationsOn your own collectionsAlways think about it

The failure mode I see most often is not underusing these features. It is a codebase where someone reached for match types and inline resolution to solve something a sealed trait handled fine, and now the compile takes four minutes and nobody wants to touch that module. The type system is good enough now that restraint is the skill worth practicing.

Thanks for reading all ten.