`match` requires explicitly listing dependencies as scrutinees or causes "type mismatch"

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider a situation like this:

inductive Nat' : Nat → Type where
  | zero : Nat' 0
  | succ (x : Nat' n) : Nat' (n + 1)

example (n : Nat) (xs : Nat' n) : Vector Nat n :=
  match xs with
  | .zero => #v[]
  | _ => sorry

Here, it suffices to specify xs and Lean automatically detects that it also needs to scrutinize n. However, there are situations in which this mechanism fails, requiring the user to tediously use _, _, _, ... in the match arms.

Context

This happened in a type theory formalization project.

Steps to Reproduce

Consider this:

inductive Expr : Nat → Type where
  | next (m : Expr n) : Expr (n + 1)

inductive X : Expr n → Type where
  | x {m : Expr n} : X (.next m)

/--
error: Type mismatch
  X.x
has type
  X (Expr.next ?m.6)
but is expected to have type
  X e
---
error: Case tag `rhs` not found.

Note: There are no cases to select.
-/
#guard_msgs in
def fails {e f : Expr n} (x : X e) :
    X f := by
  match x with
  | .x => sorry

def works {e f : Expr n} (x : X e) :
    X f := by
  match n, e, x with
  | _, _, .x => sorry

Expected behavior:

Lean should automatically match over n and e, too, and resolve the type mismatch this way.

Actual behavior:

The user gets a "type mismatch" error that e cannot be identified with .next _.

Versions

Lean 4.24.0-nightly-2025-09-02
Target: x86_64-unknown-linux-gnu

Additional Information

The symptoms of this issue look similar to this issue, except that adding more scrutinees doesn't help there.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproducer from the issue against the referenced Lean nightly version, comparing fails with works. Investigate how match x selects scrutinees for indexed inductive types such as Expr and X; the issue is done when the shorter match automatically scrutinizes n and e without the type mismatch.