Fix scala#12800: Clarify MT reduction error on empty scrutinee

Author: OlivierBlanvillain

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

@@ -13,6 +13,7 @@ object MatchTypeTrace:
     case TryReduce(scrut: Type)
     case NoMatches(scrut: Type, cases: List[Type])
     case Stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])
+    case EmptyScrutinee(scrut: Type)
   import TraceEntry._
 
   private class MatchTrace:
@@ -61,6 +62,12 @@ object MatchTypeTrace:
   def stuck(scrut: Type, stuckCase: Type, otherCases: List[Type])(using Context) =
     matchTypeFail(Stuck(scrut, stuckCase, otherCases))
 
+  /** Record a failure that scrutinee `scrut` is provably empty.
+   *  Only the first failure is recorded.
+   */
+  def emptyScrutinee(scrut: Type)(using Context) =
+    matchTypeFail(EmptyScrutinee(scrut))
+
   /** Record in the trace that we are trying to reduce `scrut` when performing `op`
    *  If `op` succeeds the entry is removed after exit. If `op` fails, it stays.
    */
@@ -91,6 +98,9 @@ object MatchTypeTrace:
          |  matches none of the cases
          |
          |    ${casesText(cases)}"""
+    case EmptyScrutinee(scrut) =>
+      i"""  failed since selector  $scrut
+         |  is uninhabited."""
     case Stuck(scrut, stuckCase, otherCases) =>
       i"""  failed since selector  $scrut
          |  does not match  ${caseText(stuckCase)}

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

@@ -2921,8 +2921,11 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       // 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)
+      if (provablyEmpty(scrut))
+        MatchTypeTrace.emptyScrutinee(scrut)
+        NoType
+      else
+        recur(cases)
     }
   }
 }

tests/neg/12800.scala

@@ -0,0 +1,21 @@
+object Test {
+  type FieldType2[K, +V] = V with KeyTag2[K, V]
+  trait KeyTag2[K, +V] extends Any
+
+  type WrapUpper = Tuple
+  type Wrap[A] = Tuple1[A]
+
+  type Extract[A <: WrapUpper] = A match {
+    case Wrap[h] => h
+  }
+
+  summon[Extract[Wrap[FieldType2["foo", Int]]] =:= FieldType2["foo", Int]] // error
+  //                                                                     ^
+  // Cannot prove that Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]] =:= Main.FieldType2[("foo" : String), Int].
+  //
+  // Note: a match type could not be fully reduced:
+  //
+  //   trying to reduce  Main.Extract[Tuple1[Main.FieldType2[("foo" : String), Int]]]
+  //   failed since selector  Tuple1[Main.FieldType2[("foo" : String), Int]]
+  //   is uninhabited.
+}