Ill-typed `match` motive inference

Prerequisites

• 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

When match generalization is off, abstracting the motive over a discriminant can lead to an ill-typed motive.

Steps to Reproduce

example (x : Nat) (y : Fin (x + 1)) : Fin (y + 2) :=
  match (generalizing := false) x with
  | 0 => 0
  | _ => 0

Expected behavior: No errors

Actual behavior: A type error saying that y has type Fin (x + 1) but is expected to have type Fin (0 + 1)

Versions

Lean 4.28.0-nightly-2026-01-12
Target: x86_64-unknown-linux-gnu

Additional Information

There is similarity to why we do discriminant refinement. I'm not blocked by this, I just noticed while playing around with match elaboration. I think it can be fixed in elabDiscrs by testing whether the type Lean.mkForall userName .default discrType (<- kabstract result.matchType discr) is type-correct. If not, fall back to a constant motive.

Impact

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

Start by reproducing the minimal example against the reported Lean nightly version, then inspect the match elaboration path around elabDiscrs. Check how the inferred motive is validated when match generalization is disabled. Done means the example elaborates without a type error and a regression test covers the case.