Refine Matchtype checking

Take up scala#13780 again, but refine it so that abstract types are allowed in match type
reduction as long as they uniquely instantiate type parameters of the type pattern.

Fixes scala#11982

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

@@ -4,6 +4,7 @@ package core
 
 import Types._, Contexts._, Symbols._, Decorators._
 import util.Property
+import Names.Name
 
 /** A utility module to produce match type reduction traces in error messages.
  */
@@ -13,6 +14,7 @@ object MatchTypeTrace:
     case TryReduce(scrut: Type)
     case NoMatches(scrut: Type, cases: List[Type])
     case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])
+    case NoInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds)
     case EmptyScrutinee(scrut: Type)
   import TraceEntry._
 
@@ -62,6 +64,9 @@ object MatchTypeTrace:
   def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) =
     matchTypeFail(Stuck(scrut, stuckCase, otherCases))
 
+  def noInstance(scrut: Type, stuckCase: Type, pname: Name, bounds: TypeBounds)(using Context) =
+    matchTypeFail(NoInstance(scrut, stuckCase, pname, bounds))
+
   /** Record a failure that scrutinee `scrut` is provably empty.
    *  Only the first failure is recorded.
    */
@@ -114,6 +119,10 @@ object MatchTypeTrace:
            |  Therefore, reduction cannot advance to the remaining case$s
            |
            |    ${casesText(otherCases)}"""
+    case NoInstance(scrut, stuckCase, pname, bounds) =>
+      i"""  failed since selector  $scrut
+         |  does not uniquely determine parameter $pname in  ${caseText(stuckCase)}
+         |  The computed bounds for the parameter are:  $bounds."""
 
   def noMatchesText(scrut: Type, cases: List[Type])(using Context): String =
     i"""failed since selector  $scrut

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

@@ -60,6 +60,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** Indicates whether the subtype check used GADT bounds */
   private var GADTused: Boolean = false
 
+  protected var canWidenAbstract: Boolean = true
+
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 
@@ -757,9 +759,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
     def tryBaseType(cls2: Symbol) = {
       val base = nonExprBaseType(tp1, cls2)
-      if (base.exists && (base `ne` tp1))
-        isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
-        base.isInstanceOf[OrType] && fourthTry
+      if base.exists && (base ne tp1)
+        && (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists)
+      then
+        isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
+        || base.isInstanceOf[OrType] && fourthTry
           // if base is a disjunction, this might have come from a tp1 type that
           // expands to a match type. In this case, we should try to reduce the type
           // and compare the redux. This is done in fourthTry
@@ -776,7 +780,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 || narrowGADTBounds(tp1, tp2, approx, isUpper = true))
               && (tp2.isAny || GADTusage(tp1.symbol))
 
-            isSubType(hi1, tp2, approx.addLow) || compareGADT || tryLiftedToThis1
+            (!caseLambda.exists || canWidenAbstract) && isSubType(hi1, tp2, approx.addLow)
+            || compareGADT
+            || tryLiftedToThis1
           case _ =>
             // `Mode.RelaxedOverriding` is only enabled when checking Java overriding
             // in explicit nulls, and `Null` becomes a bottom type, which allows
@@ -2845,7 +2851,16 @@ object TypeComparer {
     comparing(_.tracked(op))
 }
 
+object TrackingTypeComparer:
+  enum MatchResult:
+    case Reduced(tp: Type)
+    case Disjoint
+    case Stuck
+    case NoInstance(param: Name, bounds: TypeBounds)
+
 class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
+  import TrackingTypeComparer.*
+
   init(initctx)
 
   override def trackingTypeComparer = this
@@ -2883,15 +2898,25 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   }
 
   def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
-    def paramInstances = new TypeAccumulator[Array[Type]] {
-      def apply(inst: Array[Type], t: Type) = t match {
-        case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
-          inst(n) = approximation(t, fromBelow = variance >= 0).simplified
-          inst
+
+    def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
+      def apply(insts: Array[Type], t: Type) = t match
+        case param @ TypeParamRef(b, n) if b eq caseLambda =>
+          insts(n) = {
+            if canApprox then
+              approximation(param, fromBelow = variance >= 0)
+            else constraint.entry(param) match
+              case entry: TypeBounds =>
+                val lo = fullLowerBound(param)
+                val hi = fullUpperBound(param)
+                if isSubType(hi, lo) then lo else TypeBounds(lo, hi)
+              case inst =>
+                assert(inst.exists, i"param = $param\nconstraint = $constraint")
+                inst
+          }.simplified
+          insts
         case _ =>
-          foldOver(inst, t)
-      }
-    }
+          foldOver(insts, t)
 
     def instantiateParams(inst: Array[Type]) = new TypeMap {
       def apply(t: Type) = t match {
@@ -2907,7 +2932,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
      *           None         if the match fails and we should consider the following cases
      *                        because scrutinee and pattern do not overlap
      */
-    def matchCase(cas: Type): Option[Type] = trace(i"match case $cas vs $scrut", matchTypes) {
+    def matchCase(cas: Type): MatchResult = trace(i"match case $cas vs $scrut", matchTypes) {
       val cas1 = cas match {
         case cas: HKTypeLambda =>
           caseLambda = constrained(cas)
@@ -2918,34 +2943,48 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
 
       val defn.MatchCase(pat, body) = cas1: @unchecked
 
-      if (isSubType(scrut, pat))
-        // `scrut` is a subtype of `pat`: *It's a Match!*
-        Some {
-          caseLambda match {
-            case caseLambda: HKTypeLambda =>
-              val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
-              instantiateParams(instances)(body).simplified
-            case _ =>
-              body
-          }
-        }
+      def matches(canWidenAbstract: Boolean): Boolean =
+        val saved = this.canWidenAbstract
+        this.canWidenAbstract = canWidenAbstract
+        try necessarySubType(scrut, pat)
+        finally this.canWidenAbstract = saved
+
+      def redux(canApprox: Boolean): MatchResult =
+        caseLambda match
+          case caseLambda: HKTypeLambda =>
+            val instances = paramInstances(canApprox)(new Array(caseLambda.paramNames.length), pat)
+            instances.indices.find(instances(_).isInstanceOf[TypeBounds]) match
+              case Some(i) if !canApprox =>
+                MatchResult.NoInstance(caseLambda.paramNames(i), instances(i).bounds)
+              case _ =>
+                MatchResult.Reduced(instantiateParams(instances)(body).simplified)
+          case _ =>
+            MatchResult.Reduced(body)
+
+      if caseLambda.exists && 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.
-        None
+        MatchResult.Disjoint
       else
-        Some(NoType)
+        MatchResult.Stuck
     }
 
     def recur(remaining: List[Type]): Type = remaining match
       case cas :: remaining1 =>
         matchCase(cas) match
-          case None =>
+          case MatchResult.Disjoint =>
             recur(remaining1)
-          case Some(NoType) =>
+          case MatchResult.Stuck =>
             MatchTypeTrace.stuck(scrut, cas, remaining1)
             NoType
-          case Some(tp) =>
+          case MatchResult.NoInstance(pname, bounds) =>
+            MatchTypeTrace.noInstance(scrut, cas, pname, bounds)
+            NoType
+          case MatchResult.Reduced(tp) =>
             tp
       case Nil =>
         val casesText = MatchTypeTrace.noMatchesText(scrut, cases)

compiler/test/dotty/tools/dotc/CompilationTests.scala

@@ -200,6 +200,7 @@ class CompilationTests {
   @Test def runAll: Unit = {
     implicit val testGroup: TestGroup = TestGroup("runAll")
     aggregateTests(
+      compileFile("tests/run-custom-args/typeclass-derivation1.scala", defaultOptions.without(yCheckOptions*)),
       compileFile("tests/run-custom-args/tuple-cons.scala", allowDeepSubtypes),
       compileFile("tests/run-custom-args/i5256.scala", allowDeepSubtypes),
       compileFile("tests/run-custom-args/no-useless-forwarders.scala", defaultOptions and "-Xmixin-force-forwarders:false"),

tests/neg/6570-1.check

@@ -0,0 +1,30 @@
+-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------
+23 |  def thing = new Trait1 {} // error
+   |                           ^
+   |                           Found:    Object with Trait1 {...}
+   |                           Required: N[Box[Int & String]]
+   |
+   |                           Note: a match type could not be fully reduced:
+   |
+   |                             trying to reduce  N[Box[Int & String]]
+   |                             failed since selector  Box[Int & String]
+   |                             is uninhabited (there are no values of that type).
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------
+36 |  def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing  // error
+   |                                                    ^^^^^^^
+   |                                               Found:    M[T]
+   |                                               Required: Trait2
+   |
+   |                                               where:    T is a type in method foo with bounds <: Cov[Box[Int]]
+   |
+   |
+   |                                               Note: a match type could not be fully reduced:
+   |
+   |                                                 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:   >: Box[Int].
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg/6570-1.scala

@@ -33,7 +33,7 @@ class Asploder extends Root[Cov[Box[Int & String]]] {
 }
 
 object Main {
-  def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing
+  def foo[T <: Cov[Box[Int]]](c: Root[T]): Trait2 = c.thing  // error
   def explode = foo(new Asploder)
 
   def main(args: Array[String]): Unit =

tests/neg/6570.scala

@@ -21,7 +21,7 @@ object UpperBoundParametricVariant {
   trait Child[A <: Cov[Int]] extends Root[A]
 
   // we reduce `M[T]` to `Trait2`, even though we cannot be certain of that
-  def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing
+  def foo[T <: Cov[Int]](c: Child[T]): Trait2 = c.thing  // error
 
   class Asploder extends Child[Cov[String & Int]] {
     def thing = new Trait1 {} // error
@@ -42,7 +42,7 @@ object InheritanceVariant {
 
   trait Child extends Root { type B <: { type A <: Int } }
 
-  def foo(c: Child): Trait2 = c.thing
+  def foo(c: Child): Trait2 = c.thing  // error
 
   class Asploder extends Child {
     type B = { type A = String & Int }
@@ -98,7 +98,7 @@ object UpperBoundVariant {
 
   trait Child extends Root { type A <: Cov[Int] }
 
-  def foo(c: Child): Trait2 = c.thing
+  def foo(c: Child): Trait2 = c.thing  // error
 
   class Asploder extends Child {
     type A = Cov[String & Int]

tests/neg/i11982.check

@@ -0,0 +1,39 @@
+-- [E057] Type Mismatch Error: tests/neg/i11982.scala:9:34 -------------------------------------------------------------
+9 |            b: ValueOf[Tuple.Head[Tuple.Tail[X]]]  // error
+  |                                  ^
+  |                                Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
+  |
+  |                                Note: a match type could not be fully reduced:
+  |
+  |                                  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:   >: Any *: EmptyTuple.type <: Tuple.
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E057] Type Mismatch Error: tests/neg/i11982.scala:10:38 ------------------------------------------------------------
+10 |  ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] =  // error
+   |                                      ^
+   |                              Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
+   |
+   |                              Note: a match type could not be fully reduced:
+   |
+   |                                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:   >: Any *: EmptyTuple.type <: Tuple.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E057] Type Mismatch Error: tests/neg/i11982.scala:12:25 ------------------------------------------------------------
+12 |    type BB = Tuple.Head[Tuple.Tail[X]]  // error
+   |                         ^
+   |                         Type argument Tuple.Tail[X] does not conform to upper bound NonEmptyTuple
+   |
+   |                         Note: a match type could not be fully reduced:
+   |
+   |                           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:   >: Any *: EmptyTuple.type <: Tuple.
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg/i11982.scala

@@ -0,0 +1,27 @@
+package tuplefun
+object Unpair {
+
+  def pair[A, B](using a: ValueOf[A], b: ValueOf[B]): Tuple2[A, B] =
+    (a.value, b.value)
+
+  def unpair[X <: Tuple2[?, ?]](
+      using a: ValueOf[Tuple.Head[X]],
+            b: ValueOf[Tuple.Head[Tuple.Tail[X]]]  // error
+  ): Tuple2[Tuple.Head[X], Tuple.Head[Tuple.Tail[X]]] =  // error
+    type AA = Tuple.Head[X]
+    type BB = Tuple.Head[Tuple.Tail[X]]  // error
+    pair[AA, BB](using a, b)
+}
+
+object UnpairApp {
+  import Unpair._
+
+  type Tshape = ("msg", 42)
+
+  // the following won't compile when in the same file as Unpair
+  val p1: ("msg", 42) = unpair[Tshape]
+
+  @main def pairHello: Unit =
+    assert(p1 == ("msg", 42))
+    println(p1)
+}

tests/neg/i13780.check

@@ -0,0 +1,34 @@
+-- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
+18 |  def int[X <: Y]: Int = unpair[X]  // error
+   |                         ^^^^^^^^^
+   |                         Found:    Head[X]
+   |                         Required: Int
+   |
+   |                         where:    X is a type in method int with bounds <: B.this.Y
+   |
+   |
+   |                         Note: a match type could not be fully reduced:
+   |
+   |                           trying to reduce  Head[X]
+   |                           failed since selector  X
+   |                           does not uniquely determine parameter a in  case (a, b) => a
+   |                           The computed bounds for the parameter are:   >: Int.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/i13780.scala:23:37 ------------------------------------------------------------
+23 |  def string[X <: Y]: String = unpair[X]   // error
+   |                               ^^^^^^^^^
+   |                               Found:    Head[X]
+   |                               Required: String
+   |
+   |                               where:    X is a type in method string with bounds <: C.this.Y
+   |
+   |
+   |                               Note: a match type could not be fully reduced:
+   |
+   |                                 trying to reduce  Head[X]
+   |                                 failed since selector  X
+   |                                 does not uniquely determine parameter a in  case (a, b) => a
+   |                                 The computed bounds for the parameter are:   >: String.
+   |
+   | longer explanation available when compiling with `-explain`