Fix #9107: Restore constraints after MT reduction

Because of `caseLambda = constrained(cas)` in `def matchCase`, subtyping
wrongly things that it's OK to further constrain types introduced in match
type patterns. This commit fixes the issue with a stronger version of
`inFrozenConstraint` around match type reduction.

Author: OlivierBlanvillain

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/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
+}