`match` generalization failure

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

match generalization fails if the expected type is a metavariable, even though that metavariable will be assigned later on by synthesizeSyntheticMVarsUsingDefault.

Steps to Reproduce

example (a : Nat) (ha : a = 37) :=
  (match a with | 42 => by contradiction | n => n) = 37

Expected behavior: Program should be accepted

Actual behavior: Program is rejected because match generalization fails to add ha as discriminant. Manually adding ha as discriminant works.

Versions

Lean 4.27.0-rc1
Target: x86_64-unknown-linux-gnu

Additional Information

The contradiction fails because the match is not generalized.
That is because the expected type of the match is a metavariable that is not properly abstracted over a; hence the matchType is type incorrect and generalization fails to re-introduce ha : 42 = 37.

There is a "one line fix": Replacing the use of replaceFVars in Lean.Elab.Match by replaceFVarsM:

-        let type := type.replaceFVars discrs' ds'
+        let type ← type.replaceFVarsM discrs' ds'

where replaceFVarsM is defined as

/--
Replace occurrences of the free variables `fvars` in `e` with `vs`.
Similar to `Expr.replaceFVars`, but handles metavariables correctly.
-/
def _root_.Lean.Expr.replaceFVarsM (e : Expr) (fvars : Array Expr) (vs : Array Expr) : MetaM Expr :=
  return (← e.abstractM fvars).instantiateRev vs

This change does not allow motives with metavariables; later checks in the match elaborator ensure that only ground motives are handed to the match compiler.

Impact

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

Run the minimal reproducer against Lean 4.27.0-rc1, then inspect the match elaborator in Lean.Elab.Match around the replaceFVars call. Compare it with replaceFVarsM and verify that the reproducer is accepted while the existing checks for ground motives still hold.