Try just disallowing allowing widening abstract types

dwijnand · dwijnand · commit 0bc377db8879 · 2022-10-18T20:56:13.000+02:00
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/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.
diff --git a/tests/neg/11982.scala b/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"
 }
diff --git a/tests/neg/6570-1.check b/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`
diff --git a/tests/neg/i11982.check b/tests/neg/i11982.check
diff --git a/tests/neg/i11982.scala b/tests/neg/i11982.scala
diff --git a/tests/neg/i11982a.check b/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`
diff --git a/tests/neg/i13780.check b/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`
diff --git a/tests/neg/i13780.scala b/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]
 }
 
diff --git a/tests/neg/i15155.scala b/tests/neg/i15155.scala
diff --git a/tests/neg/wildcard-match.scala b/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
diff --git a/tests/pos/i15926.min.scala b/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]]
diff --git a/tests/pos/i15926.scala b/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]

Original file line number	Diff line number	Diff line change
`@@ -4,8 +4,8 @@ type Head[X] = X match {`
`4`	`4`	`}`
`5`	`5`
`6`	`6`	`object Unpair {`
`7`		`- def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1`
`8`		`- unpair[Tuple2["msg", 42]]: "msg" // error`
	`7`	`+ def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 // error`
	`8`	`+ unpair[Tuple2["msg", 42]]: "msg"`
`9`	`9`	`}`
`10`	`10`
`11`	`11`
`@@ -14,8 +14,8 @@ type Head2[X] = X match {`
`14`	`14`	`}`
`15`	`15`
`16`	`16`	`object Unpair2 {`
`17`		`- def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1`
`18`		`- unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" // error`
	`17`	`+ def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 // error`
	`18`	`+ unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg"`
`19`	`19`	`}`
`20`	`20`
`21`	`21`
`@@ -35,6 +35,6 @@ type Head4[X] = X match {`
`35`	`35`	`}`
`36`	`36`
`37`	`37`	`object Unpair4 {`
`38`		`- def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1`
`39`		`- unpair[Foo["msg", 42]]: "msg" // error`
	`38`	`+ def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 // error`
	`39`	`+ unpair[Foo["msg", 42]]: "msg"`
`40`	`40`	`}`
Original file line number	Diff line number	Diff line change
`@@ -24,9 +24,7 @@`
`24`	`24`	`\|`
`25`	`25`	`\| trying to reduce M[T]`
`26`	`26`	`\| failed since selector T`
`27`		`- \| does not uniquely determine parameter x in`
`28`		`- \| case Cov[x] => N[x]`
`29`		`- \| The computed bounds for the parameter are:`
`30`		`- \| x >: Box[Int]`
	`27`	`+ \| does not match case Cov[x] => N[x]`
	`28`	`+ \| and cannot be shown to be disjoint from it either.`
`31`	`29`	`\|`
`32`	`30`	\| longer explanation available when compiling with `-explain`
Original file line number	Diff line number	Diff line change
`@@ -9,7 +9,7 @@ trait Z {`
`9`	`9`
`10`	`10`	`class A extends Z {`
`11`	`11`	`type Y <: Tuple2[Any, Any]`
`12`		`- def unpair[X <: Y]: Head[X] = ""`
	`12`	`+ def unpair[X <: Y]: Head[X] = "" // error`
`13`	`13`	`def any[X <: Y]: Any = unpair[X]`
`14`	`14`	`}`
`15`	`15`