Refine divergence check: lexicographical order and same-size steps

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.

Author: Lluc24

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -45,14 +45,15 @@ import Capabilities.*
 import transform.Recheck.currentRechecker
 import scala.collection.immutable.HashMap
 import dotty.tools.dotc.util.Property
-import dotty.tools.dotc.reporting.NonDecreasingMatchReduction
+import dotty.tools.dotc.reporting.IncreasingMatchReduction
+import dotty.tools.dotc.reporting.CyclicMatchTypeReduction
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
 
 object Types extends TypeUtils {
 
-  val Reduction = new Property.Key[HashMap[Type, List[Int]]]
+  val Reduction = new Property.Key[HashMap[Type, List[List[Type]]]]
 
   @sharable private var nextId = 0
 
@@ -1637,20 +1638,30 @@ object Types extends TypeUtils {
         this match
           case self: AppliedType =>
             report.log(i"AppliedType with underlying MatchType: ${self.tycon}${self.args}")
-            val currentListSize = self.args.map(_.typeSize)
-            val currentSize = currentListSize.sum
-            report.log(i"Arguments Size: ${currentListSize}")
             val history = ctx.property(Reduction).getOrElse(Map.empty)
-
-            if history.contains(self.tycon) && currentSize >= history(self.tycon).sum then
-              val prevSize = history(self.tycon).sum
-              ErrorType(NonDecreasingMatchReduction(self, prevSize, currentSize))
-            else
-              val newHistory = history.updated(self.tycon, currentListSize)
-              val result =
-                given Context = ctx.fresh.setProperty(Reduction, newHistory)
-                mt.reduced.normalized
-              result
+            val decision: Either[ErrorType, List[List[Type]]] =
+              if history.contains(self.tycon) then
+                val stack = history(self.tycon) // Stack is non-empty
+                report.log(i"Match type reduction history for ${self.tycon}: $stack")
+                val currentArgsSize = self.args.map(_.typeSize)
+                val prevArgsSize = stack.head.map(_.typeSize)
+                val listOrd = scala.math.Ordering.Implicits.seqOrdering[Seq, Int]
+                if listOrd.gt(currentArgsSize, prevArgsSize) then
+                  Left(ErrorType(IncreasingMatchReduction(self.tycon, stack.head, prevArgsSize, self.args, currentArgsSize)))
+                else if listOrd.equiv(currentArgsSize, prevArgsSize) then
+                  if stack.contains(self.args) then
+                    Left(ErrorType(CyclicMatchTypeReduction(self.tycon, self.args, currentArgsSize, stack)))
+                  else Right(self.args :: stack)
+                else Right(self.args :: Nil) // currentArgsSize < prevArgsSize
+              else Right(self.args :: Nil)
+            decision match
+              case Left(err) => err
+              case Right(stack) =>
+                val newHistory = history.updated(self.tycon, stack)
+                val result =
+                  given Context = ctx.fresh.setProperty(Reduction, newHistory)
+                  mt.reduced.normalized
+                result
           case _ => mt.reduced.normalized
       case tp: AppliedType => tp.tryCompiletimeConstantFold
       case _ => NoType

compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala

@@ -236,7 +236,8 @@ enum ErrorMessageID(val isActive: Boolean = true) extends java.lang.Enum[ErrorMe
   case DefaultShadowsGivenID // errorNumber: 220
   case RecurseWithDefaultID // errorNumber: 221
   case EncodedPackageNameID // errorNumber: 222
-  case NonDecreasingMatchReductionID // errorNumber: 223
+  case IncreasingMatchReductionID // errorNumber: 223
+  case CyclicMatchTypeReductionID // errorNumber: 224
 
   def errorNumber = ordinal - 1
 

compiler/src/dotty/tools/dotc/reporting/messages.scala

@@ -3321,9 +3321,29 @@ class MatchTypeLegacyPattern(errorText: String)(using Context) extends TypeMsg(M
   def msg(using Context) = errorText
   def explain(using Context) = ""
 
-class NonDecreasingMatchReduction(tpe: Type, originalSize: Int, newSize: Int)(using Context)
-  extends TypeMsg(NonDecreasingMatchReductionID):
-  def msg(using Context) = i"Match type reduction failed: Non-decreasing argument size detected for $tpe. Size went from $originalSize to $newSize."
+class IncreasingMatchReduction(tpcon: Type, prevArgs: List[Type], prevSize: List[Int], curArgs: List[Type], curSize: List[Int])(using Context)
+  extends TypeMsg(IncreasingMatchReductionID):
+  def msg(using Context) =
+    i"""Match type reduction failed due to potentially infinite recursion.
+       |
+       |The reduction step for $tpcon resulted in strictly larger arguments (lexicographically):
+       |  Previous: $prevArgs (size: $prevSize)
+       |  Current:  $curArgs (size: $curSize)
+       |
+       |To guarantee termination, recursive match types must strictly decrease in size
+       |or stay the same (without cycles)."""
+  def explain(using Context) = ""
+
+class CyclicMatchTypeReduction(tpcon: Type, args: List[Type], argsSize: List[Int], stack: List[List[Type]])(using Context)
+  extends TypeMsg(CyclicMatchTypeReductionID):
+  def msg(using Context) =
+    val trace: String = stack.map(a => i"${tpcon}${a}").mkString(" -> ")
+    i"""Match type reduction failed due to a cycle.
+       |
+       |The match type $tpcon reduced to itself with the same arguments:
+       |$args
+       |
+       |Trace: $trace"""
   def explain(using Context) = ""
 
 class ClosureCannotHaveInternalParameterDependencies(mt: Type)(using Context)

tests/neg/i22587-neg-A.scala

@@ -1,9 +1,12 @@
-// Test Case 2: Direct Self-Reference Without Reduction (NEGATIVE)
-// This SHOULD diverge because Loop[X] immediately expands to Loop[X]
-// with no progress made - infinite loop without termination
+// Negative Test Case A: Direct Self-Reference Without Reduction
+// This SHOULD diverge because Loop[Int] => Loop[Float] => Loop[Double] => Loop[String] => Loop[Int] => ...
+// The type cycles without reaching a base case.
 
 type Loop[X] = X match
-  case Int => Loop[Int]
+  case Int => Loop[Float]
+  case Float => Loop[Double]
+  case Double => Loop[String]
+  case String => Loop[Int]
   case _ => String
 
 @main def test02(): Unit =

tests/neg/i22587-neg-B.scala

@@ -1,4 +1,4 @@
-// Test Case 3: Wrapping Type Without Progress (NEGATIVE)
+// Negative Test Case 2: Wrapping Type Without Progress
 // This SHOULD diverge because Wrap[Int] => Wrap[List[Int]] => Wrap[List[List[Int]]] => ...
 // The type grows infinitely without reaching a base case
 

tests/neg/i22587-neg-C.scala

@@ -1,7 +1,12 @@
-// Test Case 1: Simple Recursive Deconstruction (POSITIVE)
+// Positive Test Case A: Simple Recursive Deconstruction
 // This should NOT diverge because recursion always reduces the type structure
 // by unwrapping one layer (Option[t] -> t)
 
+type DoubleUnwrap[X, Y] = (X, Y) match
+  case (AnyVal, Y) => (X, Unwrap[Y])
+  case (X, AnyVal) => (Unwrap[X], Y)
+  case (X, Y) => (Unwrap[X], Unwrap[Y])
+
 type Unwrap[X] = X match
   case Option[t] => Unwrap[t]
   case _ => X
@@ -10,9 +15,9 @@ type Unwrap[X] = X match
   val e1: Unwrap[Option[Option[Int]]] = 42
   println("Test 1 - Simple recursive unwrapping:")
   println(s"e1 value: $e1")
-  
-  val e2: Unwrap[Option[String]] = "hello"
+
+  val e2: DoubleUnwrap[Option[String], Option[Int]] = ("hello", 42)
   println(s"e2 value: $e2")
-  
-  val e3: Unwrap[Int] = 99
+
+  val e3: DoubleUnwrap[Int, Int] = (1, 2)
   println(s"e3 value: $e3")

tests/pos/i22587-pos-A.scala

@@ -1,21 +1,13 @@
-// Test Case 4: Two-Parameter Match Type with Swapping (POSITIVE)
-// This should NOT diverge because even though parameters swap positions,
-// the tuple structure reduces (Tuple2 -> single type)
+// Positive Test Case B: Binary Recursive construction
+// This should NOT diverge because although types have same complexity, the structure
+// changes by incrementing by one the numeric parameter until reaching a base case.
 
-type Swap[X, Y] = (X, Y) match
-  case (Int, String) => Y
-  case (String, Int) => X
-  case (List[a], b) => Swap[a, b]
-  case (a, List[b]) => Swap[a, b]
-  case _ => X
+
+type Increase[X, Y, Z] = (X, Y, Z) match
+  case (X, Y, 0) => Increase[X, Y, 1]
+  case (X, 0, _) => Increase[X, 1, 0]
+  case (0, _, _) => Increase[1, 0, 0]
+  case _ => "done"
 
 @main def test04(): Unit =
-  val e1: Swap[Int, String] = "result"
-  println("Test 4 - Two-parameter swap:")
-  println(s"e1 value: $e1")
-  
-  val e2: Swap[String, Int] = "swapped"
-  println(s"e2 value: $e2")
-  
-  val e3: Swap[List[List[Int]], List[String]] = "42"
-  println(s"e3 value: $e3")
+  val e1: Increase[0, 0, 0] = "done"