diff --git a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
index 30bd3c168269..6874f087c017 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeApplications.scala
@@ -135,6 +135,15 @@ object TypeApplications {
     }
 
     def apply(t: Type): Type = t match {
+      case t @ AppliedType(tycon, args1) if tycon.isRef(defn.MatchCaseClass) =>
+        // Match-type case patterns and case bodies are both invariant, unsafe
+        // positions for wildcard substitution. Substituting a wildcard here
+        // either makes a pattern spuriously match anything (for a top-level
+        // param in a pattern) or loses the relationship between occurrences
+        // (for a param used multiple times in a body). See issue #21013.
+        // Force nested-level treatment so wildcard substitution is skipped,
+        // leaving the AppliedType to be flagged by `isUnreducibleWild`.
+        t.derivedAppliedType(apply(tycon), args1.mapConserve(arg => atNestedLevel(apply(arg))))
       case t @ AppliedType(tycon, args1) if tycon.typeSymbol.isClass =>
         t.derivedAppliedType(apply(tycon), args1.mapConserve(applyArg))
       case t @ RefinedType(parent, name, TypeAlias(info)) =>
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index e528143d20fc..ce380c075dbb 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -4795,15 +4795,44 @@ object Types extends TypeUtils {
       else super.tryNormalize
 
     /** Is this an unreducible application to wildcard arguments?
-     *  This is the case if tycon is higher-kinded. This means
-     *  it is a subtype of a hk-lambda, but not a match alias.
-     *  (normal parameterized aliases are removed in `appliedTo`).
+     *  This is the case if tycon is higher-kinded and at least one argument
+     *  is a wildcard, *unless* tycon is either:
+     *    - the pseudo match alias `compiletime.ops.int.S`, or
+     *    - a match alias whose wildcard arguments correspond only to type
+     *      parameters that appear solely in the match scrutinee.
+     *  (Normal parameterized aliases are removed in `appliedTo`.)
      *  Applications of higher-kinded type constructors to wildcard arguments
      *  are equivalent to existential types, which are not supported.
+     *
+     *  For match type aliases we restrict the exemption: substituting a
+     *  wildcard for a type parameter is unsound whenever that parameter
+     *  occurs in a pattern (because pattern captures would then see a
+     *  wildcard-refinable type), in a case body, or in the declared upper
+     *  bound. Only parameters used exclusively in the scrutinee are safe,
+     *  since in that case `M[?]` is simply an unreducible match type.
+     *  See issue #21013.
      */
     def isUnreducibleWild(using Context): Boolean =
-      tycon.isLambdaSub && hasWildcardArg && !isMatchAlias
-        && !(args.sizeIs == 1 && defn.isCompiletime_S(tycon.typeSymbol)) // S is a pseudo Match Alias
+      if !tycon.isLambdaSub || !hasWildcardArg then false
+      else if args.sizeIs == 1 && defn.isCompiletime_S(tycon.typeSymbol) then false
+      else matchAliasLambda match
+        case lam: HKTypeLambda => unsoundMatchAliasWildcardArgs(lam, args)
+        case _ => true
+
+    /** If this application is (the eta-expansion of) a match type alias,
+     *  returns the underlying `HKTypeLambda` whose `resType` is a `MatchType`.
+     *  Otherwise returns `NoType`. Used by `isUnreducibleWild` so that sound
+     *  wildcard applications of match aliases (the parameter only appears in
+     *  the scrutinee) can be accepted, while unsound ones are rejected.
+     */
+    private def matchAliasLambda(using Context): Type = tycon match
+      case tr: TypeRef => tr.info match
+        case MatchAlias(l: HKTypeLambda) => l
+        case _ => NoType
+      case l: HKTypeLambda => l.resType match
+        case _: MatchType => l
+        case _ => NoType
+      case _ => NoType
 
     def tryCompiletimeConstantFold(using Context): Type =
       if myEvalRunId == ctx.runId then myEvalued
@@ -7317,4 +7346,27 @@ object Types extends TypeUtils {
   private val keepIfRefining: AnnotatedType => Context ?=> Boolean = _.isRefining
 
   val isBounds: Type => Boolean = _.isInstanceOf[TypeBounds]
+
+  /** Does applying `lam` (the HKTypeLambda body of a match alias) to `args`
+   *  yield an unsound wildcard application? The application is unsound iff
+   *  `lam.resType` is a `MatchType` and some wildcard argument (a `TypeBounds`)
+   *  corresponds to a lambda parameter that occurs outside the match scrutinee
+   *  — i.e., in the match's declared upper bound, in any case pattern, or in
+   *  any case body. See issue #21013 for the motivation: substituting `?` for
+   *  a type parameter in such a position is analogous to the classic
+   *  `type U[X] = (X, X); type V = U[?]` unsoundness.
+   */
+  def unsoundMatchAliasWildcardArgs(lam: HKTypeLambda, args: List[Type])(using Context): Boolean =
+    lam.resType match
+      case mt: MatchType =>
+        val collector = new TypeAccumulator[Set[Int]]:
+          def apply(acc: Set[Int], tp: Type): Set[Int] = tp match
+            case tp: TypeParamRef if tp.binder eq lam => acc + tp.paramNum
+            case _ => foldOver(acc, tp)
+        val unsafe = mt.cases.foldLeft(collector(Set.empty, mt.bound))(collector(_, _))
+        unsafe.nonEmpty && args.iterator.zipWithIndex.exists {
+          case (_: TypeBounds, i) => unsafe.contains(i)
+          case _ => false
+        }
+      case _ => false
 }
diff --git a/docs/_spec/03-types.md b/docs/_spec/03-types.md
index 5d4e205aace9..cd348094d61f 100644
--- a/docs/_spec/03-types.md
+++ b/docs/_spec/03-types.md
@@ -1155,6 +1155,14 @@ For ´n \geq 1´, it is specified as:
 
 The reduction of an "empty" match type `´X´ match { }` (which cannot be written in user programs) is a compile error.
 
+#### Applications to Wildcard Arguments
+
+Let `´M´` be a _match type alias_ of the form `type ´M´[´a_1´, ..., ´a_n´] = ´X´ match { case ´P_1´ => ´R_1´; ...; case ´P_k´ => ´R_k´ }` (optionally with a declared upper bound).
+An application `´M´[´T_1´, ..., ´T_n´]` where some `´T_i´` is a wildcard type argument is legal only if every such `´a_i´` occurs exclusively in the scrutinee `´X´` — i.e., it does not occur in the declared upper bound, in any pattern `´P_j´`, or in any body `´R_j´`.
+
+If a wildcard is substituted for a parameter that appears in a pattern, the pattern may spuriously match scrutinees that no non-wildcard substitution would match.
+If a wildcard is substituted for a parameter that appears multiple times in a body (or in the declared upper bound), the resulting type loses the identification between those occurrences, which is the same unsoundness as substituting a wildcard for `X` in `[X] =>> (X, X)`.
+
 ### Skolem Types
 
 ```ebnf
diff --git a/tests/neg/i21013.scala b/tests/neg/i21013.scala
new file mode 100644
index 000000000000..54df1b5afd3c
--- /dev/null
+++ b/tests/neg/i21013.scala
@@ -0,0 +1,25 @@
+// Issue #21013: applying a match type alias to a wildcard argument is
+// unsound when the type parameter appears outside the match scrutinee
+// (in a pattern, a case body, or the declared upper bound).
+
+type M1[K] = Double match
+  case K => Int // K appears in a pattern
+
+type M2[K] = Double match
+  case Option[K] => Int // K appears in a pattern
+
+type M3[X, Y] = X match
+  case Int => (Y, Y) // Y appears in a case body
+
+type M4[K, S] <: List[K] = S match // K appears in the declared upper bound
+  case Int => List[K]
+
+def Test: Unit =
+  val x1: M1[?] = ??? // error
+  val x2: M2[?] = ??? // error
+  val x3: M3[Int, ?] = ??? // error
+  val x4: M4[?, String] = ??? // error
+
+  // The unsoundness observed in #21013: M1[?] should not be a valid
+  // supertype of M1[Int]. With the fix, M1[?] itself is rejected.
+  // (If it were accepted, M1[?] would reduce to Int, but M1[Int] would not.)
diff --git a/tests/pos/i21013.scala b/tests/pos/i21013.scala
new file mode 100644
index 000000000000..c41cd9e9d1a0
--- /dev/null
+++ b/tests/pos/i21013.scala
@@ -0,0 +1,34 @@
+// Companion to tests/neg/i21013.scala: wildcard applications of match
+// type aliases are sound, and must be accepted, when every wildcarded
+// parameter occurs only in the scrutinee of the underlying match type.
+
+// Sound: parameter only in scrutinee (single case)
+type Ok1[X] = X match
+  case Int => String
+
+val a1: Ok1[?] = ???
+def b1: Ok1[?] = ???
+val c1: List[Ok1[?]] = Nil
+val d1: Option[Ok1[?]] = None
+
+// Sound: parameter only in scrutinee (multiple cases, default)
+type Ok2[X] = X match
+  case Int => String
+  case String => Int
+  case _ => Double
+
+val a2: Ok2[?] = ???
+def b2: Array[Ok2[?]] = null
+
+// Sound mix: the wildcarded parameter only appears in the scrutinee,
+// the other parameter is given concretely and may appear anywhere.
+type Ok3[X, Y] = X match
+  case Int => (Y, Y)
+  case String => List[Y]
+
+val a3: Ok3[?, Int] = ???
+def b3: Ok3[?, String] = ???
+
+// Bounded wildcard, still sound
+def b4: Ok1[? <: Int] = ???
+def b5: Ok2[? >: Nothing <: Int | String] = ???