Bug in replaceLocalDeclDefEq

[djvelleman]

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean.MVarId.replaceLocalDeclDefEq doesn't do anything if the new type for the FVar happens to equal the type of the goal

Steps to Reproduce

Here is an example that illustrates the problem:

elab "test" h:ident : tactic => do let g ← Lean.Elab.Tactic.getMainGoal g.withContext do let ldec ← Lean.Meta.getLocalDeclFromUserName h.getId let f := ldec.fvarId let e ← Lean.Meta.whnf (← Lean.instantiateMVars ldec.type) let newgoal ← g.replaceLocalDeclDefEq f e Lean.Elab.Tactic.replaceMainGoal [newgoal]

example (n : Nat) (h : 2 ∣ n) : ∃ c, n = c * 2 := by test h

example (n : Nat) (h : 2 ∣ n) : ∃ c, n = 2 * c := by test h

Expected behavior: In both cases, the type of h should change to ∃ c, n = 2 * c

Actual behavior: It changes in the first example, but not the second

Reproduces how often: Always

Versions

Lean (version 4.0.0-nightly-2022-08-25, commit d4799eaf3a74, Release) MacOS 12.5.1

Additional Information

It is clear what the bug is: The test "if typeNew == mvarDecl.type then" is the wrong test. Should be comparing typeNew to the type of the fvar, not the type of the mvar.