rw adding rather than replacing a hypothesis

[hrmacbeth]

Prerequisites

• 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

When the tactic rw is used to change the type of a hypothesis h, it generally does this by replacing h with the new (rewritten) version. It should only keep both versions of the hypothesis (new and old) if the old version was referred to somewhere in the context.

In the following example, the keep-both behaviour occurs, but the old version of h doesn't seem to appear anywhere in the context. This only happens when a certain type argument is implicit.

Steps to Reproduce

theorem explicit (α) [OfNat α 0] (a b : α) : (a = b) = (a = 0) := sorry
theorem implicit {α} [OfNat α 0] (a b : α) : (a = b) = (a = 0) := sorry

variable (a b : Nat) (h : a = b)

-- desirable behaviour: replaces h
example : False := by
  rw [explicit] at h
  sorry

-- undesirable behaviour: does not replace h
example : False := by
  rw [implicit] at h
  sorry

Expected behavior:

The two examples should generate the same goal state,

a b : Nat
h : a = 0
⊢ False

Actual behavior:

In the second example the old version of h has not been overwritten:

a b : Nat
h✝ : a = b
h : a = 0
⊢ False

Reproduces how often: 100%

Versions

nightly-2023-03-15

Additional Information

Zulip

Per @digama0

There must be something hidden in the context which is referring to the old h .... probably the thing that is referring to the old h is a metavariable which is not yet solved (e.g. the variable α in foo)

[hrmacbeth]

This is now fixed. I bisected and the fix seems to date to nightly-2023-10-25, so perhaps #2712 or #2728 fixed it.