diff --git a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala b/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
index 054b445432a8..f711f8d1ab67 100644
--- a/compiler/src/dotty/tools/dotc/core/MatchTypeTrace.scala
+++ b/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 (there are no values of that type)."""
     case Stuck(scrut, stuckCase, otherCases) =>
       i"""  failed since selector  $scrut
          |  does not match  ${caseText(stuckCase)}
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 38fd65cb4c54..033d26301df1 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/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)
     }
   }
 }
diff --git a/tests/neg/12800.scala b/tests/neg/12800.scala
new file mode 100644
index 000000000000..164276396bec
--- /dev/null
+++ b/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.
+}
diff --git a/tests/neg/matchtype-seq.check b/tests/neg/matchtype-seq.check
index b5dc6923d374..c2207fa1aea3 100644
--- a/tests/neg/matchtype-seq.check
+++ b/tests/neg/matchtype-seq.check
@@ -257,6 +257,8 @@ longer explanation available when compiling with `-explain`
     |                                        Note: a match type could not be fully reduced:
     |
     |                                          trying to reduce  Test.T9[(Nothing, String)]
+    |                                          failed since selector  (Nothing, String)
+    |                                          is uninhabited (there are no values of that type).
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:106:40 ----------------------------------------------------
@@ -268,6 +270,8 @@ longer explanation available when compiling with `-explain`
     |                                        Note: a match type could not be fully reduced:
     |
     |                                          trying to reduce  Test.T9[(String, Nothing)]
+    |                                          failed since selector  (String, Nothing)
+    |                                          is uninhabited (there are no values of that type).
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:107:37 ----------------------------------------------------
@@ -279,6 +283,8 @@ longer explanation available when compiling with `-explain`
     |                                     Note: a match type could not be fully reduced:
     |
     |                                       trying to reduce  Test.T9[(Int, Nothing)]
+    |                                       failed since selector  (Int, Nothing)
+    |                                       is uninhabited (there are no values of that type).
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:108:37 ----------------------------------------------------
@@ -290,6 +296,8 @@ longer explanation available when compiling with `-explain`
     |                                     Note: a match type could not be fully reduced:
     |
     |                                       trying to reduce  Test.T9[(Nothing, Int)]
+    |                                       failed since selector  (Nothing, Int)
+    |                                       is uninhabited (there are no values of that type).
 
 longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/matchtype-seq.scala:109:29 ----------------------------------------------------