Implement strict size-decreasing divergence check for Match Types

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 #22587.

Author: Lluc24

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

@@ -43,12 +43,17 @@ import cc.*
 import CaptureSet.IdentityCaptRefMap
 import Capabilities.*
 import transform.Recheck.currentRechecker
+import scala.collection.immutable.HashMap
+import dotty.tools.dotc.util.Property
+import dotty.tools.dotc.reporting.NonDecreasingMatchReduction
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
 
 object Types extends TypeUtils {
 
+  val Reduction = new Property.Key[HashMap[Type, List[Int]]]
+
   @sharable private var nextId = 0
 
   implicit def eqType: CanEqual[Type, Type] = CanEqual.derived
@@ -1628,7 +1633,25 @@ object Types extends TypeUtils {
      *  then the result after applying all toplevel normalizations, otherwise NoType.
      */
     def tryNormalize(using Context): Type = underlyingNormalizable match
-      case mt: MatchType => mt.reduced.normalized
+      case mt: MatchType =>
+        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
+          case _ => mt.reduced.normalized
       case tp: AppliedType => tp.tryCompiletimeConstantFold
       case _ => NoType
 

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

@@ -236,6 +236,7 @@ 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
 
   def errorNumber = ordinal - 1
 

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

@@ -3321,6 +3321,11 @@ 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."
+  def explain(using Context) = ""
+
 class ClosureCannotHaveInternalParameterDependencies(mt: Type)(using Context)
   extends TypeMsg(ClosureCannotHaveInternalParameterDependenciesID):
     def msg(using Context) =

tests/neg/i22587-neg-A.scala

@@ -0,0 +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
+
+type Loop[X] = X match
+  case Int => Loop[Int]
+  case _ => String
+
+@main def test02(): Unit =
+  val e1: Loop[Int] = ??? // error
+  println("Test 2 - Direct self-reference:")
+  println(s"e1 value: $e1")

tests/neg/i22587-neg-B.scala

@@ -0,0 +1,12 @@
+// Test Case 3: Wrapping Type Without Progress (NEGATIVE)
+// This SHOULD diverge because Wrap[Int] => Wrap[List[Int]] => Wrap[List[List[Int]]] => ...
+// The type grows infinitely without reaching a base case
+
+type Wrap[X] = X match
+  case AnyVal => Wrap[List[X]]
+  case AnyRef => Wrap[List[X]]
+
+@main def test03(): Unit =
+  val e1: Wrap[Int] = ??? // error
+  println("Test 3 - Wrapping without progress:")
+  println(s"e1 value: $e1")

tests/neg/i22587-neg-C.scala

@@ -0,0 +1,14 @@
+// Test Case 5: Two-Parameter Match Type with Swapping (Negative)
+// This should diverge because even though recursion should reduce,
+// the sum of parameters size does not decrease in one recursive step.
+
+type Swap[X, Y] = (X, Y) match
+  case (Int, String) => Swap[Y, X]
+  case (String, Int) => X
+  case (List[a], b) => Swap[a, b]
+  case (a, List[b]) => Swap[a, b]
+  case _ => X
+
+@main def test05(): Unit =
+  val e: Swap[List[List[Int]], List[String]] = ??? // error
+  println(s"e value: $e")

tests/pos/i22587-pos-A.scala

@@ -0,0 +1,18 @@
+// Test Case 1: Simple Recursive Deconstruction (POSITIVE)
+// This should NOT diverge because recursion always reduces the type structure
+// by unwrapping one layer (Option[t] -> t)
+
+type Unwrap[X] = X match
+  case Option[t] => Unwrap[t]
+  case _ => X
+
+@main def test01(): Unit =
+  val e1: Unwrap[Option[Option[Int]]] = 42
+  println("Test 1 - Simple recursive unwrapping:")
+  println(s"e1 value: $e1")
+  
+  val e2: Unwrap[Option[String]] = "hello"
+  println(s"e2 value: $e2")
+  
+  val e3: Unwrap[Int] = 99
+  println(s"e3 value: $e3")

tests/pos/i22587-pos-B.scala

@@ -0,0 +1,21 @@
+// 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)
+
+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
+
+@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")