Pre-SIP: Divergence Checking for Match Type Reduction

Scala Improvement Process
1

Pre-SIP: Divergence Checking for Match Type Reduction

Issue: #22587
Implementation PR: #24661
Full report & proof: Lluc24/divergence

Situation

Match types can diverge during reduction — either cycling through a closed set of types or growing complexity without bound. The compiler currently lets reduction run until it hits a StackOverflowError, which it then catches to report a “recursion limit exceeded” error.

Catching StackOverflowError is fundamentally unsafe. The JVM specification does not guarantee correct cleanup after a stack overflow: documented OpenJDK bugs confirm that finally blocks can be bypassed (JDK-8177802), locks can remain held after recovery (JDK-8318888), and behavior is platform- and -Xss-dependent (JDK-8217475).

Proposed solution

Replace the runtime stack-overflow heuristic with a compile-time divergence check that proves termination before reduction proceeds.

The algorithm adapts the divergence check from SIP-31 (Byname Implicit Parameters) — which already handles this for implicit resolution — and extends it from single types to full argument lists. For each match type constructor the compiler tracks the sequence of argument lists seen during reduction and rejects a new argument list when it is dominated by a previously seen one.

Domination is defined as follows. Given an argument list T:

  • Complexity vector c(T): the size of a type measured using the structural AST of each argument.
  • Covering set cs(T): the union of all type symbols mentioned in the arguments.

T is dominated by a history entry U when either:

  1. T and U are type-equivalent (cycle detection), or
  2. cs(T) = cs(U) and c(T) is component-wise strictly larger than c(U) (growth detection).

When domination is detected the compiler throws a MatchTypeDivergence exception — caught at the same site as RecursionOverflow — and emits a clear error with the full reduction trace, complexity vectors, and covering sets.

Termination proof

The algorithm is proven to terminate by three lemmas:

  1. Finite covering sets — only finitely many covering sets can arise.
  2. Non-decreasing subsequence — every infinite sequence in ℕⁿ contains a non-decreasing subsequence (generalized Dickson’s Lemma).
  3. Finite constructible types — a fixed covering set and fixed complexity vector admit only finitely many distinct types (Pigeonhole Principle).

By contradiction: any infinite reduction sequence would either trigger growth detection (Lemmas 1 + 2) or cycle detection (Lemma 3).

The full formal proof is available in the project report.

Implementation status

The implementation is complete and ready to be merged. All existing Scala 3 compiler tests pass without modification — the check is conservative enough to accept every match type that compiled before.

This project was directed by Martin Odersky and supervised by Matthieu Bovel. It was presented in person to the LAMP research group, who endorsed it for the SIP track.

9 Likes
2

Why do we need a SIP for this? It is a compiletime error instead of a runtime exception. Isn’t it more of an implementation detail?

3

Behind the implementation there is a complex formal proof. I presented in person to Martin Odersky and the LAMP group who endorsed for the SIP. It would define rigorously the mathematical abstractions of the algorithm.

4

This I understood. What I don’t understand is why there is need for a change in spec. Before this change we have this type of code won't work, but we can't prove it, and now we have this type of code won't work, and we can prove it. From user perspective the code doesn’t work anyways and suddenly applying the change can’t be really seen as a regression, IMO (expecting an exception and instead getting a compiler error).

1 Like
5

If just a PR on the compiler is enough then that’s a faster track to inclusion than via the SIP process. I think that may be a question for the chair @etaconversion

6

:backhand_index_pointing_up:

That’s already been decided. Such excellent work should be enshrined as a SIP. Also, how else could I put my dear SIP committee to work?

2 Likes
7

Are we sure the old and new logic are equivalent ?

For example, are there cases where the older system would reduce something which cannot be proven to terminate ?

2 Likes
8

Also, how else could I put my dear SIP committee to work?

Haha - happy that you put us to work on such excellent progress like this! (Not sure I’m the most able to add anything on the review of the underlying formalisms, but I’d be glad to review the benefits and vote on approval.)

9

Then please do share with rest of the class as to why.

10
  1. Martin Odersky supervised this, and was satisfied enough to suggest making a SIP.
  2. The SIP process is open to anyone.
  3. You seem to have a problem with it. I am happy to hear your counterarguments at one of the next SIP meetings, once a SIP document is presented.
11

Do we know if there are match types out in the wild, which currently compile, but will no longer do so with this?

1 Like
12

Have not even implied otherwise.

This a pre sip discussion and no one wants to discuss my question. That’s my only problem.

13

: cries in Pre-SIP: Divergence Checking for Match Type Reduction - #7 by Sporarum :

14

:slight_smile:

I was referring to the people who know why this is a SIP and not need to guess.

15

The usual rule of thumb is that if a change involves changing the language specification, then it needs a SIP.

In practice,

  • Sufficiently small and uncontroversial changes don’t need SIP, like if something is essentially just a bugfix or clarification in the spec

But also, and more relevantly here,

  • We are free to choose to ask for the SIP committee’s input if something isn’t covered in the language spec but is deemed sufficiently important or interesting or potentially controversial (so e.g. changing scala to run Scala-CLI went through the SIP committee)
1 Like
16

I think this way of stating it may be causing some confusion. If I understand correctly, “runtime” in this sentence, and elsewhere in your post, is still something that’s happening at compile-time…?

Normally we only call something a “runtime error” if it occurs when user code runs, rather than when user code is compiled.

2 Likes
17

Yes, both stack-overflow heuristic and the divergence check are compile-time. Sorry about the confusion - I will clarify in the PR. It doesn’t allow me to edit this post anymore

1 Like
18

Potentially yes. There are some known controversial cases documented in the Discussion section of the LAMP presentation here.

19

The SIP defines rigorous, concrete rules for match-type reduction. This is potentially controversial because the check is sound but conservative: it can reject types that actually terminate. For example, this Sapeless3 pattern:

type Tail [ X ] = X match
    case _ *: t = > t

type Apply [ C [ _ ] , T ] = T match
    case h *: _ = > C [ h ] *: Apply [C , Tail [ T ]]
    case EmptyTuple = > EmptyTuple

type Solve = Apply [ Option , ( Int , Int ) ]

Match-types arguments are unreduced, so the compiler sees:

Step 1: T ⇒ size N
Step 2: Tail[T] ⇒ size N + 1
Step 3: Tail[Tail[T]] ⇒ size N + 2

So the argument looks like it grows without bound, because the check can’t use the fact that Tail shrinks a concrete tuple — that only holds once the tuple is reduced. Hence, a false positive. We apply a grace threshold to recover cases like this and keep the full community build green.

Other patterns (e.g. compiletime.ops) are discussed in the Discussion section of the LAMP presentation here.

3 Likes
20

Thank you. That is what I was looking for.

2 Likes