A subtle detail about Lean `rw` tactic

Stream: new members

[Shuhao Song]

Hello! I'm new to the Lean community. I spent almost whole forenoon time trying to understand some subtle behavior of rw tactic. Consider the following example code:

axiom α : Type
axiom β : Type
axiom p : α → Prop
axiom q : α → Prop
axiom r : α → Prop
axiom rp : {x : α} → r x ↔ p x
axiom rq : {x : α} → r x ↔ q x
axiom f : (x : α) → p x → β
axiom g : (x : α) → q x → β
axiom y : β
axiom fx : (x : α) → (hx : r x) → f x (rp.mp hx) = g x (rq.mp hx)
example (x : α) (hx : r x) : g x (rq.mp hx) = y := by
  have test : y = f x (rp.mp hx) := by sorry
  have test₂ : 0 = 0 := by rfl
  rw [fx _] at test
  exact test.symm

The exact test.symm reports an error:

application type mismatch
  Eq.symm test
argument
  test
has type
  y = g x ⋯ : Prop
but is expected to have type
  y = ?m.184 : Prop

That may seem strange, because the metavariable ?m.184 can be unified with g x. So why the assignment step failed? I read the Lean source code trying to understand it. The rw tactic changes a hypothesis (FVar) called test, and because the original hypothesis can't be safely deleted, it was daggered (test✝). However, after rw, the FVar test₂ was then became a new FVar with different FVarId but the same name (test₂), that may be the reason.
The hole in rw [fx _] at test creates a new metavariable, say ?m.149 (thats the value in https://live.lean-lang.org). The expression g x ... contains the metavariable ?m.149, and it will be assigned to ?m.184. In function processAssignment of file Lean.Meta.ExprDefEq, it will call checkAssignment to check if an expression can be assigned to a metavariable, and if not it will try first-order unification (processAssignmentFOApprox and then processConstApprox).
In checkAssignment, it will use checkMVar to check if a metavariable (like ?m.149, we use $p$ to denote it) is suitable for assignmented to another metavariable (like ?m.184, use $q$ to denote). If the context of $p$ is part of current context (to speak rigorously, "part of" means function Lean.LocalContext.isSubPrefixOf), the check would succeed. If config.ctxApprox is true and the current context is part of context of p, it also succeeds. However, it's not both the case: ?m.149 has context test and test₂, the current context is test (display with dagger), test(new, rewrited) and test₂. Note that two test₂ have different FVarId, so neither context are part of each other.
Then it is easy to understand why the exact test.symm would succeed, if you remove have test₂ : 0 = 0 := by rfl, even these two tactics seems not relevant to each other.

[Shuhao Song]

Can we modify the implementation of rw to make this better?

[Eric Wieser]

I think this example might be worth filing as a bug report.

[Eric Wieser]

let n := 1 is also enough to trigger the issue, instead of have test₂ : 0 = 0 := by rfl

[Eric Wieser]

Even more surprisingly, have test2 := test instead of exact test.symm still fails!

[Shuhao Song]

Yes because it modifies the local context. The difference of have and let is just .cdecl and .ldecl in LocalDecl type, so they don't difference a lot.

Eric Wieser said:

let n := 1 is also enough to trigger the issue, instead of have test₂ : 0 = 0 := by rfl

[Shuhao Song]

Eric Wieser said:

I think this example might be worth filing as a bug report.

How can I submit a bug report?

[Shuhao Song]

Eric Wieser said:

have test2 := test

Because it need to fill the metavariable of type of test2.

[Eric Wieser]

github.com/leanprover/lean4/issues