Force MT reduction simplification, disallow infinite match types

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

@@ -3201,7 +3201,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
                   }
                 }
               case redux =>
-                MatchResult.Reduced(redux.simplified)
+                MatchResult.Reduced(redux)
           case _ =>
             MatchResult.Reduced(body)
 
@@ -3229,7 +3229,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
             MatchTypeTrace.noInstance(scrut, cas, fails)
             NoType
           case MatchResult.Reduced(tp) =>
-            tp
+            tp.simplified
       case Nil =>
         val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
         ErrorType(reporting.MatchTypeNoCases(casesText))

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

@@ -359,7 +359,7 @@ object Types {
      *  (since these are relevant for inference or resolution) but never consider prefixes
      *  (since these often do not constrain the search space anyway).
      */
-    def unusableForInference(using Context): Boolean = widenDealias match
+    def unusableForInference(using Context): Boolean = try widenDealias match
       case AppliedType(tycon, args) => tycon.unusableForInference || args.exists(_.unusableForInference)
       case RefinedType(parent, _, rinfo) => parent.unusableForInference || rinfo.unusableForInference
       case TypeBounds(lo, hi) => lo.unusableForInference || hi.unusableForInference
@@ -369,6 +369,7 @@ object Types {
       case CapturingType(parent, refs) => parent.unusableForInference || refs.elems.exists(_.unusableForInference)
       case _: ErrorType => true
       case _ => false
+    catch case ex: Throwable => handleRecursive("unusableForInference", show, ex)
 
     /** Does the type carry an annotation that is an instance of `cls`? */
     @tailrec final def hasAnnotation(cls: ClassSymbol)(using Context): Boolean = stripTypeVar match {

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -198,7 +198,7 @@ object Inferencing {
         case tp => foldOver(x, tp)
       }
       catch case ex: Throwable =>
-        handleRecursive("check fully defined", tp.show, ex)
+        handleRecursive("check fully defined", tp.showSummary(20), ex)
     }
 
     def process(tp: Type): Boolean =

compiler/test/dotty/tools/repl/ReplCompilerTests.scala

@@ -169,6 +169,62 @@ class ReplCompilerTests extends ReplTest:
       )
     }
 
+  @Test def i16596 =
+    initially {
+      run("""
+        |import scala.compiletime.{error, ops, requireConst}, ops.int.*
+        |import scala.quoted.*
+        |
+        |sealed trait Nat
+        |object Nat:
+        |  case object Zero extends Nat
+        |  case class Succ[N <: Nat](prev: N) extends Nat
+        |
+        |  given zero: Zero.type = Zero
+        |  given buildSucc[N <: Nat](using n: N): Succ[N] = Succ(n)
+        |
+        |  def value[N <: Nat](using n: N): N = n
+        |
+        |  def prevImpl[I <: Int: Type](expr: Expr[I])(using Quotes): Expr[I - 1] =
+        |    val prev = expr.valueOrAbort - 1
+        |    // this compiles, but fails at use time
+        |    //Expr(prev).asExprOf[ops.int.-[I, 1]]
+        |    Expr(prev).asInstanceOf[Expr[I - 1]]
+        |
+        |  inline def prevOf[I <: Int](inline i: I): I - 1 = ${prevImpl('i)}
+        |
+        |  type FromInt[I <: Int] <: Nat = I match
+        |     case 0 => Zero.type
+        |     case _ => Succ[FromInt[I - 1]]
+        |
+        |  inline def fromInt[I <: Int & Singleton](i: I): FromInt[i.type] =
+        |    requireConst(i)
+        |    inline i match
+        |      case _: 0 => Zero
+        |      case _ =>
+        |        inline if i < 0
+        |        then error("cannot convert negative to Nat")
+        |        else Succ(fromInt(prevOf[i.type](i)))
+      """.stripMargin)
+    }.andThen {
+      assertEquals(
+        """// defined trait Nat
+          |// defined object Nat
+          |""".stripMargin, storedOutput())
+      run("Nat.fromInt(2)")
+    }.andThen {
+      assertEquals("val res0: Nat.Succ[Nat.Succ[Nat.Zero.type]] = Succ(Succ(Zero))", storedOutput().trim)
+      run("summon[Nat.FromInt[2]]")
+    }.andThen {
+      assertEquals("val res1: Nat.Succ[Nat.Succ[Nat.Zero.type]] = Succ(Succ(Zero))", storedOutput().trim)
+      run("Nat.fromInt(3)")
+    }.andThen {
+      assertEquals("val res2: Nat.Succ[Nat.Succ[Nat.Succ[Nat.Zero.type]]] = Succ(Succ(Succ(Zero)))", storedOutput().trim)
+      run("summon[Nat.FromInt[3]]")
+    }.andThen {
+      assertEquals("val res3: Nat.Succ[Nat.Succ[Nat.Succ[Nat.Zero.type]]] = Succ(Succ(Succ(Zero)))", storedOutput().trim)
+    }
+
   @Test def i6200 =
     initially {
       run("""

tests/neg-custom-args/isInstanceOf/i17435.scala

@@ -14,10 +14,10 @@ object Test:
   type JsonArray = mutable.Buffer[Json]
 
   def encode(x: Json): Int = x match
-    case str: String => 1
-    case b: Boolean => 2
-    case i: Int => 3
-    case d: Double => 4
+    case str: String => 1       // error
+    case b: Boolean => 2        // error
+    case i: Int => 3            // error
+    case d: Double => 4         // error
     case arr: JsonArray => 5    // error
     case obj: JsonObject => 6   // error
     case _ => 7

tests/pos/i15158.scala → tests/neg/i15158.scala

@@ -13,9 +13,9 @@ val x = foo {
   type Rec[A] = A match
     case String => Opt[Rec[String]]
 
-  val arr = new Buf[Rec[String]](8)
-  val arr2 = Buf[Rec[String]](8)
-  val arr3 = Buf.apply[Rec[String]](8)
+  val arr = new Buf[Rec[String]](8)    // error
+  val arr2 = Buf[Rec[String]](8)       // error
+  val arr3 = Buf.apply[Rec[String]](8) // error
 }
 
 import scala.collection.mutable
@@ -38,6 +38,6 @@ class Spec {
       JsonPrimitive
     ]
 
-    val arr = new mutable.ArrayBuffer[Json](8)
+    val arr = new mutable.ArrayBuffer[Json](8) // error
   }
 }

tests/neg/mt-recur.cov.scala

@@ -0,0 +1,7 @@
+// like mt-recur.scala, but covariant
+class Cov[+T]
+
+type Recur[X] = X match
+  case Int => Cov[Recur[X]]
+
+def x = ??? : Recur[Int] // error

tests/neg/mt-recur.scala

@@ -0,0 +1,10 @@
+// an example of an infinite recursion match type
+// using an _invariant_ type constructor
+// see mt-recur.cov.scala for covariant
+// used to track the behaviour of match type reduction
+class Inv[T]
+
+type Recur[X] = X match
+  case Int => Inv[Recur[X]]
+
+def x = ??? : Recur[Int] // error

tests/pos/i16596.more.scala

@@ -0,0 +1,35 @@
+import scala.compiletime.ops.int.*
+
+object NatExample {
+  sealed trait Nat
+  object Nat {
+    case object Zero extends Nat
+    case class Succ[N <: Nat](prev: N) extends Nat
+
+    given zero: Zero.type = Zero
+    given buildSucc[N <: Nat](using n: N): Succ[N] = Succ(n)
+
+    def value[N <: Nat](using n: N): N = n
+
+    type FromInt[I <: Int] <: Nat = I match
+      case 0 => Zero.type
+      case _ => Succ[FromInt[I - 1]]
+
+    summon[FromInt[0] =:= Zero.type]
+    summon[FromInt[1] =:= Succ[Zero.type]]
+    summon[FromInt[2] =:= Succ[Succ[Zero.type]]]
+    summon[FromInt[3] =:= Succ[Succ[Succ[Zero.type]]]]
+    summon[FromInt[4] =:= Succ[Succ[Succ[Succ[Zero.type]]]]]
+
+    @main def test = {
+      require(summon[FromInt[0]] == Zero)
+      require(summon[FromInt[1]] == Succ(Zero))
+      require(summon[FromInt[2]] == Succ(Succ(Zero)))
+      require(summon[FromInt[3]] == Succ(Succ(Succ(Zero))))
+      // we can summon 4 if we write it out:
+      require(summon[Succ[Succ[Succ[Succ[Zero.type]]]]] == Succ(Succ(Succ(Succ(Zero)))))
+      // was: we cannot summon 4 using the match type
+      require(summon[FromInt[4]] == Succ(Succ(Succ(Succ(Zero)))))
+    }
+  }
+}

tests/pos/i16596.orig.scala

@@ -0,0 +1,28 @@
+import scala.compiletime.ops.int
+
+type Count0[N,T] <: Tuple = (N,T) match
+  case (0,_)      => EmptyTuple
+  case (N,String) => String *: Count0[int.-[N, 1], String]
+  case (N,Int)    => Int *: Count0[int.-[N, 1], Int]
+  case (N,Float)  => Float *: Count0[int.-[N, 1], Float]
+  case (N,Double) => Double *: Count0[int.-[N, 1], Double]
+
+
+type Count1[N,T] <: Tuple = (N,T) match
+  case (0,T)      => EmptyTuple
+  case (N,String) => String *: Count1[int.-[N, 1], String]
+  case (N,Int)    => Int *: Count1[int.-[N, 1], Int]
+  case (N,Float)  => Float *: Count1[int.-[N, 1], Float]
+  case (N,Double) => Double *: Count1[int.-[N, 1], Double]
+
+def t01 = summon[Count0[1, Int] =:= Int *: EmptyTuple ]
+def t02 = summon[Count0[2, Int] =:= Int *: Int *: EmptyTuple]
+def t03 = summon[Count0[3, Int] =:= Int *: Int *: Int *: EmptyTuple]
+def t04 = summon[Count0[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple]
+def t05 = summon[Count0[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple]
+
+def t11 = summon[Count1[1, Int] =:= Int *: EmptyTuple ]
+def t12 = summon[Count1[2, Int] =:= Int *: Int *: EmptyTuple]
+def t13 = summon[Count1[3, Int] =:= Int *: Int *: Int *: EmptyTuple] // was: Fail from here
+def t14 = summon[Count1[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple]
+def t15 = summon[Count1[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple]

tests/pos/i16596.scala

@@ -0,0 +1,14 @@
+import scala.compiletime.ops.int, int.-
+
+type Count[N, T] <: Tuple = (N, T) match
+  case (0, T) => EmptyTuple
+  case (N, T) => T *: Count[N - 1, T]
+
+val a: Count[3, Int] = (1, 2, 3)
+val b: Count[4, Int] = (1, 2, 3, 4)
+val c: Count[5, Int] = (1, 2, 3, 4, 5)
+val d: Count[6, Int] = (1, 2, 3, 4, 5, 6)
+val z: Count[23, Int] = (
+  1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
+  11, 12, 13, 14, 15, 16, 17, 18, 19, 20,
+  21, 22, 23)

tests/pos/i17257.min.scala

@@ -0,0 +1,16 @@
+// scalac: -Yno-deep-subtypes:false
+// Minimisation of tests/run-macros/i17257
+// to understand how changes to match type reduction
+// impacted this use of Tuple.IsMappedBy.
+//
+// During match type reduction
+// if we do NOT simplify the case lambda parameter instances
+// then this large tuple make TypeComparer breach LogPendingSubTypesThreshold
+// which, under -Yno-deep-subtypes, crashes the compilation.
+class C[+A]
+def foo[T <: Tuple : Tuple.IsMappedBy[C]] = ???
+def bar[X] = foo[(
+  C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X],
+  C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X], C[X],
+  C[X], C[X], C[X],
+)]