Ill-typed `match` motive inference

[sgraf812]

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.