Fix #9107: Restore constraints after MT reduction

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

@@ -2848,25 +2848,32 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         MatchTypeTrace.noMatches(scrut, cases)
         NoType
 
-    inFrozenConstraint {
-      // Empty types break the basic assumption that if a scrutinee and a
-      // pattern are disjoint it's OK to reduce passed that pattern. Indeed,
-      // empty types viewed as a set of value is always a subset of any other
-      // types. As a result, we first check that the scrutinee isn't empty
-      // before proceeding with reduction. See `tests/neg/6570.scala` and
-      // `6570-1.scala` for examples that exploit emptiness to break match
-      // type soundness.
-
-      // If we revered the uncertainty case of this empty check, that is,
-      // `!provablyNonEmpty` instead of `provablyEmpty`, that would be
-      // obviously sound, but quite restrictive. With the current formulation,
-      // we need to be careful that `provablyEmpty` covers all the conditions
-      // used to conclude disjointness in `provablyDisjoint`.
-      if (provablyEmpty(scrut))
-        NoType
-      else
-        recur(cases)
+    // inFrozenConstraint is not sufficient here as it doesn't prevent
+    // parameters of type lambdas from being added to `constraint`, see
+    // ConstraintHandling.canConstrain and tests/neg/9107.scala.
+    val saved = constraint
+    try {
+      inFrozenConstraint {
+        // Empty types break the basic assumption that if a scrutinee and a
+        // pattern are disjoint it's OK to reduce passed that pattern. Indeed,
+        // empty types viewed as a set of value is always a subset of any other
+        // types. As a result, we first check that the scrutinee isn't empty
+        // before proceeding with reduction. See `tests/neg/6570.scala` and
+        // `6570-1.scala` for examples that exploit emptiness to break match
+        // type soundness.
+
+        // If we reversed the uncertainty case of this empty check, that is,
+        // `!provablyNonEmpty` instead of `provablyEmpty`, that would be
+        // obviously sound, but quite restrictive. With the current formulation,
+        // we need to be careful that `provablyEmpty` covers all the conditions
+        // used to conclude disjointness in `provablyDisjoint`.
+        if (provablyEmpty(scrut))
+          NoType
+        else
+          recur(cases)
+      }
     }
+    finally constraint = saved
   }
 }
 

tests/pos/6697.scala → tests/neg/6697-1.scala

@@ -3,5 +3,6 @@ object Test {
   case class Of[sup, sub <: sup]() extends Off
   type Sup[O <: Off] = O match { case Of[sup, sub] => sup }
   type Sub[O <: Off] = O match { case Of[sup, sub] => sub }
-  type Copy[O <: Off] = Of[Sup[O], Sub[O]]
+  type Copy[O <: Off] = Of[Sup[O], Sub[O]] // error
+  // Type argument Test.Sub[O] does not conform to upper bound Test.Sup[O]
 }

tests/neg/6697-2.scala

@@ -0,0 +1,18 @@
+object Test {
+  sealed trait Off
+  case class Of[sup, sub <: sup]() extends Off
+
+  def sup[O <: Off](o: O) = o match {
+    case _: Of[sup, sub] =>
+      val a: sub = null.asInstanceOf
+      // Even though we know that sub <: sup from Of's bounds, that knowledge
+      // is lost in the body of pattern matching expressions...
+
+      val b: sup = a // error
+      //  Found:    (a : sub)
+      //  Required: sup
+      //  where:    sub is a type in method sup with bounds <: Test.Of[?, ?]#sup
+
+      ()
+  }
+}

tests/neg/9107.scala

@@ -0,0 +1,14 @@
+trait M[F[_]]
+trait Inv[T]
+
+object Test {
+  def ev[X] = implicitly[
+    (X match { case Inv[t] => Int }) =:=
+    (X match { case Inv[t] => t })
+  ] // error
+
+  def ev2[X] = implicitly[
+    (M[[t] =>> runtime.MatchCase[Inv[t], Int]])  =:=
+    (M[[t] =>> runtime.MatchCase[Inv[t], t]])
+  ] // error
+}

tests/pos/9890.scala

@@ -0,0 +1,49 @@
+object Test {
+  import scala.compiletime.ops.int._
+
+  trait x
+
+  type Range[Min <: Int, Max <: Int] <: Tuple = Min match {
+    case Max => EmptyTuple
+    case _ => Min *: Range[Min + 1, Max]
+  }
+
+  type TupleMap[Tup <: Tuple, Bound, F[_ <: Bound]] <: Tuple = Tup match {
+    case EmptyTuple => EmptyTuple
+    case h *: t => F[h] *: TupleMap[t, Bound, F]
+  }
+  type TupleDedup[Tup <: Tuple, Mask] <: Tuple = Tup match {
+    case EmptyTuple => EmptyTuple
+    case h *: t => h match {
+      case Mask => TupleDedup[t, Mask]
+      case _ => h *: TupleDedup[t, h | Mask]
+    }
+  }
+
+  type CoordToPos[r <: Int, c <: Int] = r * 9 + c
+  type Cell[r <: Int, c <: Int, Board <: Tuple] = Tuple.Elem[Board, CoordToPos[r, c]]
+  type Col[c <: Int, Board <: Tuple] = TupleMap[Range[0, 9], Int, [r <: Int] =>> Cell[r, c, Board]]
+
+  type ColFromPos[Pos <: Int] = Pos % 9
+
+  type Sudoku1 = (
+    x, x, x,  x, 1, x,  4, x, 6,
+    8, x, 1,  6, 2, x,  x, x, 9,
+    x, 3, x,  x, x, 9,  x, 2, x,
+
+    5, x, 9,  1, 3, x,  x, 6, x,
+    x, 6, x,  9, x, 2,  x, 4, x,
+    x, 2, x,  x, 6, 7,  8, x, 5,
+
+    x, 9, x,  5, x, x,  x, 3, x,
+    3, x, x,  x, 4, 6,  9, x, 7,
+    6, x, 7,  x, 9, x,  x, x, x,
+  )
+
+  //compiles fine
+  summon[Col[ColFromPos[0], Sudoku1] =:= (x, 8, x,  5, x, x,  x, 3, 6)]
+
+  summon[TupleDedup[(x, 8, x,  5, x, x,  x, 3, 6), Nothing] =:= (x, 8, 5, 3, 6)]
+  //but this doesn't
+  summon[TupleDedup[Col[ColFromPos[0], Sudoku1], Nothing] =:= (x, 8, 5, 3, 6)]
+}