diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index dc54d14b0d4b..feb3739efa2c 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -43,12 +43,18 @@ 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.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[List[Type]]]]
+
   @sharable private var nextId = 0
 
   implicit def eqType: CanEqual[Type, Type] = CanEqual.derived
@@ -1628,7 +1634,35 @@ 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 history = ctx.property(Reduction).getOrElse(Map.empty)
+            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
 
diff --git a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
index 5f5a0c01db17..35b3026bf9da 100644
--- a/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/ErrorMessageID.scala
@@ -236,6 +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 IncreasingMatchReductionID // errorNumber: 223
+  case CyclicMatchTypeReductionID // errorNumber: 224
 
   def errorNumber = ordinal - 1
 
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 159b3c9a905e..e1f7cb41d29e 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -3321,6 +3321,31 @@ class MatchTypeLegacyPattern(errorText: String)(using Context) extends TypeMsg(M
   def msg(using Context) = errorText
   def explain(using Context) = ""
 
+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)
   extends TypeMsg(ClosureCannotHaveInternalParameterDependenciesID):
     def msg(using Context) =
diff --git a/tests/neg/i22587-neg-A.scala b/tests/neg/i22587-neg-A.scala
new file mode 100644
index 000000000000..aa2d51c556b5
--- /dev/null
+++ b/tests/neg/i22587-neg-A.scala
@@ -0,0 +1,15 @@
+// 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[Float]
+  case Float => Loop[Double]
+  case Double => Loop[String]
+  case String => Loop[Int]
+  case _ => String
+
+@main def test02(): Unit =
+  val e1: Loop[Int] = ??? // error
+  println("Test 2 - Direct self-reference:")
+  println(s"e1 value: $e1")
diff --git a/tests/neg/i22587-neg-B.scala b/tests/neg/i22587-neg-B.scala
new file mode 100644
index 000000000000..d01b2189350d
--- /dev/null
+++ b/tests/neg/i22587-neg-B.scala
@@ -0,0 +1,12 @@
+// 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
+
+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")
diff --git a/tests/pos/i22587-pos-A.scala b/tests/pos/i22587-pos-A.scala
new file mode 100644
index 000000000000..78e309a3db29
--- /dev/null
+++ b/tests/pos/i22587-pos-A.scala
@@ -0,0 +1,23 @@
+// 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
+
+@main def test01(): Unit =
+  val e1: Unwrap[Option[Option[Int]]] = 42
+  println("Test 1 - Simple recursive unwrapping:")
+  println(s"e1 value: $e1")
+
+  val e2: DoubleUnwrap[Option[String], Option[Int]] = ("hello", 42)
+  println(s"e2 value: $e2")
+
+  val e3: DoubleUnwrap[Int, Int] = (1, 2)
+  println(s"e3 value: $e3")
diff --git a/tests/pos/i22587-pos-B.scala b/tests/pos/i22587-pos-B.scala
new file mode 100644
index 000000000000..0681398546bf
--- /dev/null
+++ b/tests/pos/i22587-pos-B.scala
@@ -0,0 +1,13 @@
+// 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 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: Increase[0, 0, 0] = "done"