diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index a8d27c6448c8..1b58dd8c1dbc 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -3353,6 +3353,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
        * upper bound of an abstract type.
        *
        * See notably neg/wildcard-match.scala for examples of this.
+       *
+       * See neg/i13780.scala and neg/i13780-1.scala for ClassCastException
+       * reproducers if we disable this check.
        */
 
       def followEverythingConcrete(tp: Type): Type =
diff --git a/tests/neg/i13780-1.check b/tests/neg/i13780-1.check
new file mode 100644
index 000000000000..029ef3f3ac4b
--- /dev/null
+++ b/tests/neg/i13780-1.check
@@ -0,0 +1,39 @@
+-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:38:24 ----------------------------------------------------------
+38 |    case x: (h *: t) => x.head // error
+   |                        ^^^^^^
+   |                      Found:    Tuple.Head[VS & h *: t]
+   |                      Required: h
+   |
+   |                      where:    VS is a type in method foo with bounds <: Tuple
+   |                                h  is a type in method foo with bounds 
+   |                                t  is a type in method foo with bounds <: Tuple
+   |
+   |
+   |                      Note: a match type could not be fully reduced:
+   |
+   |                        trying to reduce  Tuple.Head[VS & h *: t]
+   |                        failed since selector VS & h *: t
+   |                        does not uniquely determine parameter x in
+   |                          case x *: _ => x
+   |                        The computed bounds for the parameter are:
+   |                          x <: h
+   |                      Note that implicit conversions were not tried because the result of an implicit conversion
+   |                      must be more specific than h
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:52:31 ----------------------------------------------------------
+52 |  def unpair: SelectH[Y & W] = "" // error
+   |                               ^^
+   |                               Found:    ("" : String)
+   |                               Required: SelectH[A.this.Y & A.this.W]
+   |
+   |                               Note: a match type could not be fully reduced:
+   |
+   |                                 trying to reduce  SelectH[A.this.Y & A.this.W]
+   |                                 failed since selector A.this.Y & A.this.W
+   |                                 does not uniquely determine parameter h in
+   |                                   case h *: _ => h
+   |                                 The computed bounds for the parameter are:
+   |                                   h
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/i13780-1.scala b/tests/neg/i13780-1.scala
new file mode 100644
index 000000000000..39f06e520797
--- /dev/null
+++ b/tests/neg/i13780-1.scala
@@ -0,0 +1,69 @@
+/* It is tempting to relax the `isConcrete` test of match types for `AndType`
+ * in the following way:
+ *
+ * (isConcrete(tp.tp1) || !tp.tp1.derivesFrom(targetClass)) && (... same for tp.tp2)
+ *
+ * but the test in this file shows that this would be unsound.
+ *
+ * If we did relax the rule, it would help usages of match types applied to the
+ * singleton type of term pattern match scrutinees. For example:
+ *
+ * def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
+ *   case x: (h *: t) => x.head
+ *
+ * The type of `x` in the branch body is `(VS & (h *: t))`. The result of
+ * `x.head` is therefore a `Tuple.Head[VS & (h *: t)]`, which does not reduce
+ * according to the current rules, but would reduce to `h` with the relaxed
+ * rule.
+ *
+ * Note that the code can be fixed with an explicit type argument to `.head`:
+ *
+ * def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
+ *   case x: (h *: t) => x.head[h *: t]
+ *
+ * So it *seems* like it would be fine to relax the rule, based on the insight
+ * that `VS` in `Tuple.Head[VS & (h *: t)]` does not contribute anything to the
+ * computed type capture in `Tuple.Head`.
+ *
+ * The test is this file demonstrates that relaxing the rule can cause
+ * unsoundness. So don't do it.
+ */
+
+type SelectH[VS <: Tuple] = VS match
+  case h *: ? => h
+
+// The original example found in the fingo/spata library
+object ExampleFromSpata:
+  def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
+    case x: (h *: t) => x.head // error
+
+  def bar[VS <: Tuple](x: VS): SelectH[VS] = x match
+    case x: (h *: t) => x.head[h *: t] // ok
+end ExampleFromSpata
+
+trait Z {
+  type Y <: Tuple
+  type W <: Tuple
+  def unpair: SelectH[Y & W]
+}
+
+class A extends Z {
+  type Y = Tuple2[Any, Any]
+  def unpair: SelectH[Y & W] = "" // error
+  def any: Any = unpair
+}
+
+class B extends A { this: Z =>
+  type W = Tuple2[Int, Int]
+  def int: Int = unpair
+}
+
+class C extends A { this: Z =>
+  type W = Tuple2[String, String]
+  def string: String = unpair
+}
+
+object Main {
+  def main(args: Array[String]): Unit =
+    println((new B).int + 1) // would give ClassCastException
+}