Try just disallowing widening of abstract types

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

@@ -3134,10 +3134,8 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
           case _ =>
             MatchResult.Reduced(body)
 
-      if caseLambda.exists && matches(canWidenAbstract = false) then
+      if matches(canWidenAbstract = false) then
         redux(canApprox = true)
-      else if matches(canWidenAbstract = true) then
-        redux(canApprox = false)
       else if (provablyDisjoint(scrut, pat))
         // We found a proof that `scrut` and `pat` are incompatible.
         // The search continues.

tests/neg/11982.scala

@@ -4,8 +4,8 @@ type Head[X] = X match {
 }
 
 object Unpair {
-  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1
-  unpair[Tuple2["msg", 42]]: "msg"  // error
+  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 // error
+  unpair[Tuple2["msg", 42]]: "msg"
 }
 
 
@@ -14,8 +14,8 @@ type Head2[X] = X match {
 }
 
 object Unpair2 {
-  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1
-  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" // error
+  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 // error
+  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg"
 }
 
 
@@ -35,6 +35,6 @@ type Head4[X] = X match {
 }
 
 object Unpair4 {
-  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1
-  unpair[Foo["msg", 42]]: "msg" // error
+  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 // error
+  unpair[Foo["msg", 42]]: "msg"
 }

tests/neg/6570-1.check

@@ -24,9 +24,7 @@
    |
    |                                                  trying to reduce  M[T]
    |                                                  failed since selector  T
-   |                                                  does not uniquely determine parameter x in
-   |                                                    case Cov[x] => N[x]
-   |                                                  The computed bounds for the parameter are:
-   |                                                    x >: Box[Int]
+   |                                                  does not match  case Cov[x] => N[x]
+   |                                                  and cannot be shown to be disjoint from it either.
    |
    | longer explanation available when compiling with `-explain`

tests/neg/i11982a.check

@@ -7,10 +7,8 @@
   |
   |                                    trying to reduce  Tuple.Tail[X]
   |                                    failed since selector  X
-  |                                    does not uniquely determine parameter xs in
-  |                                      case _ *: xs => xs
-  |                                    The computed bounds for the parameter are:
-  |                                      xs >: Any *: EmptyTuple.type <: Tuple
+  |                                    does not match  case _ *: xs => xs
+  |                                    and cannot be shown to be disjoint from it either.
   |
   | longer explanation available when compiling with `-explain`
 -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:10:38 -----------------------------------------------------------
@@ -22,10 +20,8 @@
    |
    |                                        trying to reduce  Tuple.Tail[X]
    |                                        failed since selector  X
-   |                                        does not uniquely determine parameter xs in
-   |                                          case _ *: xs => xs
-   |                                        The computed bounds for the parameter are:
-   |                                          xs >: Any *: EmptyTuple.type <: Tuple
+   |                                        does not match  case _ *: xs => xs
+   |                                        and cannot be shown to be disjoint from it either.
    |
    | longer explanation available when compiling with `-explain`
 -- [E057] Type Mismatch Error: tests/neg/i11982a.scala:12:25 -----------------------------------------------------------
@@ -37,9 +33,7 @@
    |
    |                           trying to reduce  Tuple.Tail[X]
    |                           failed since selector  X
-   |                           does not uniquely determine parameter xs in
-   |                             case _ *: xs => xs
-   |                           The computed bounds for the parameter are:
-   |                             xs >: Any *: EmptyTuple.type <: Tuple
+   |                           does not match  case _ *: xs => xs
+   |                           and cannot be shown to be disjoint from it either.
    |
    | longer explanation available when compiling with `-explain`

tests/neg/i13780.check

@@ -1,3 +1,20 @@
+-- [E007] Type Mismatch Error: tests/neg/i13780.scala:12:32 ------------------------------------------------------------
+12 |  def unpair[X <: Y]: Head[X] = "" // error
+   |                                ^^
+   |                                Found:    ("" : String)
+   |                                Required: Head[X]
+   |
+   |                                where:    X is a type in method unpair with bounds <: A.this.Y
+   |
+   |
+   |                                Note: a match type could not be fully reduced:
+   |
+   |                                  trying to reduce  Head[X]
+   |                                  failed since selector  X
+   |                                  does not match  case (a, b) => a
+   |                                  and cannot be shown to be disjoint from it either.
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
 18 |  def int[X <: Y]: Int = unpair[X]  // error
    |                         ^^^^^^^^^
@@ -11,11 +28,8 @@
    |
    |                           trying to reduce  Head[X]
    |                           failed since selector  X
-   |                           does not uniquely determine parameters a, b in
-   |                             case (a, b) => a
-   |                           The computed bounds for the parameters are:
-   |                             a >: Int
-   |                             b >: Int
+   |                           does not match  case (a, b) => a
+   |                           and cannot be shown to be disjoint from it either.
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------
@@ -31,10 +45,7 @@
    |
    |                                 trying to reduce  Head[X]
    |                                 failed since selector  X
-   |                                 does not uniquely determine parameters a, b in
-   |                                   case (a, b) => a
-   |                                 The computed bounds for the parameters are:
-   |                                   a >: String
-   |                                   b >: String
+   |                                 does not match  case (a, b) => a
+   |                                 and cannot be shown to be disjoint from it either.
    |
    | longer explanation available when compiling with `-explain`

tests/neg/i13780.scala

@@ -9,7 +9,7 @@ trait Z {
 
 class A extends Z {
   type Y <: Tuple2[Any, Any]
-  def unpair[X <: Y]: Head[X] = ""
+  def unpair[X <: Y]: Head[X] = "" // error
   def any[X <: Y]: Any = unpair[X]
 }
 

tests/pos/i15155.scala → tests/neg/i15155.scala

@@ -7,5 +7,5 @@ type EnumValue[A <: Enumeration] = A match {
 
 // https://github.com/json4s/json4s/blob/355d8751391773e0d79d04402a4f9fb7bfc684ec/ext/src/main/scala/org/json4s/ext/EnumSerializer.scala#L25-L26
 class EnumSerializer[E <: Enumeration: ClassTag](enumeration: E) {
-  val EnumerationClass = classOf[EnumValue[E]]
-}
+  val EnumerationClass = classOf[EnumValue[E]] // error
+}

tests/neg/wildcard-match.scala

@@ -24,17 +24,17 @@ type ContravToList[X] = X match
 class C
 
 def f[X <: Box[C], Y <: Cov[C], Z <: Contrav[C]] =
-  def a: BoxElem[X] = ???  // OK
-  val _: C = a
+  def a: BoxElem[X] = ???
+  val _: C = a // error
 
   def a1: CovElem[Y] = ???
   val _: C = a1  // error
 
   def a2: ContravElem[Z] = ???
   val _: C = a2  // error
 
-  def b: BoxToList[X] = ???  // OK
-  val _: List[C] = b
+  def b: BoxToList[X] = ???
+  val _: List[C] = b // error
 
   def b1: CovToList[Y] = ???
   val _: List[C] = b1  // error

tests/pos/i15926.min.scala

@@ -0,0 +1,19 @@
+sealed trait Nat
+final case class Zero() extends Nat
+final case class Succ[+N <: Nat]() extends Nat
+
+final case class Neg[+N <: Succ[Nat]]()
+
+type Sum[X, Y] = Y match
+  case Zero    => X
+  case Succ[y] => Sum[Succ[X], y]
+
+type IntSum[A, B] = B match
+  case Neg[b] => A match
+    case Neg[a] => Neg[Sum[a, b]]
+
+type One = Succ[Zero]
+type Two = Succ[One]
+
+class Test:
+  def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]]

tests/pos/i15926.scala

@@ -0,0 +1,27 @@
+@main def main(): Unit =
+  println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]])
+
+sealed trait IntT
+sealed trait NatT extends IntT
+final case class Zero() extends NatT
+final case class Succ[+N <: NatT](n: N) extends NatT
+final case class Minus[+N <: Succ[NatT]](n: N) extends IntT
+
+type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
+  case Zero => X
+  case Succ[y] => NatSum[Succ[X], y]
+
+type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match
+  case Zero => X
+  case Succ[y] => X match
+    case Zero => Minus[Y]
+    case Succ[x] => NatDif[x, y]
+
+type Sum[X <: IntT, Y <: IntT] <: IntT = Y match
+  case Zero => X
+  case Minus[y] => X match
+    case Minus[x] => Minus[NatSum[x, y]]
+    case _ => NatDif[X, y]
+  case _ => X match
+    case Minus[x] => NatDif[Y, x]
+    case _ => NatSum[X, Y]