Skip to content

Conversation

@Lluc24
Copy link
Contributor

@Lluc24 Lluc24 commented Dec 4, 2025

Closes #22587: Implement Divergence Checking for Match Types

  • Addresses the issue where match type reduction relies on catching StackOverflowError to handle infinite recursion, which is unsafe and slow.
  • Adapts the "Open Implicits" divergence checking algorithm (from SIP-31) to ApplyTypes and MatchTypes.
  • Introduces a new Property in the Context to track the history of types currently being reduced.
  • Enforces termination by verifying that arguments of the Match Type do not increase in size compared to previous reductions in the history.
  • Returns a standard Error Type when divergence is detected.

@mbovel mbovel self-requested a review December 4, 2025 10:43
case AnyVal => Wrap[List[Int]]

@main def test03(): Unit =
val e1: Wrap[Int] = ??? // error
Copy link
Member

@bishabosha bishabosha Dec 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

List[Int] is not AnyVal , so then it stops there right?

Copy link
Contributor Author

@Lluc24 Lluc24 Dec 6, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're absolutely right. I've fixed the test case.

The divergence check currently applies even to match types that do not strictly reduce (stuck matches). Instead of simply stopping and returning NoType (or the stuck type), the algorithm detects the increasing size of the scrutinee and correctly returns an ErrorType.

Thanks for the catch! I would have missed that otherwise.

This is the first step towards implementing the full divergence check
algorithm for Match Types. The logic enforces that recursive reduction
steps must have a strictly smaller size than the sum of the type sizes
of the scrutinee.

This check applies to match types during reduction as well as those
that do not reduce. When the algorithm detects a non-decreasing size,
it returns an ErrorType to prevent infinite recursion.

This work is part of the research project specified by Martin Odersky
in issue scala#22587.
@Lluc24 Lluc24 force-pushed the i22587-divergence-check-MT branch from 7de6009 to 3423338 Compare December 6, 2025 12:42
This commit relaxes the previous strict size-decreasing constraint for
Match Type reduction, allowing for more expressive recursive types while
maintaining termination guarantees.

Key changes:
1. Lexicographical Comparison: Instead of comparing the sum of argument
   sizes, the algorithm now compares the list of argument sizes
   lexicographically. This provides a more precise metric for progress.

2. Bounded Variation: Reductions are no longer required to strictly
   decrease in size at every step. Same-size reductions are now allowed,
   provided the sequence of arguments has not been seen before in the
   current reduction chain (cycle detection).

3. History Stack: A stack of previously seen argument lists is maintained
   for the current size baseline.
   - If size strictly decreases: The stack is cleared (progress made).
   - If size increases: An ErrorType is returned (divergence).
   - If size is equal: The arguments are checked against the stack.
     Repeating arguments trigger a cycle error; new arguments are added
     to the stack.

Since the number of type combinations is finite, disallowing growth
while preventing cycles guarantees the algorithm will eventually terminate.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Implement Divergence Checking for Match Types

2 participants