RPC error in `rw at *`

Stream: lean4

[Thomas Zhu]

This example triggers an RPC error Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.9'.:

import Mathlib.Data.Nat.Basic

example : True := by
  rw [le_antisymm _ _] at *

I'm not sure if this is specific to le_antisymm or something else. Removing the import makes the InternalError go away. Is this the expected behavior?

An example of where one would use such a rewrite is

import Mathlib.Data.Nat.Basic

example (a b : ℕ) (hab : a ≤ b) (hba : b ≤ a)
    (h1 : a ≥ 2) (h2 : a ≤ 3) : b ≥ 2 ∧ b ≤ 3 := by
  rw [le_antisymm hab hba] at *
  exact ⟨h1, h2⟩

[Thomas Zhu]

The second example fails with the Rpc error, but also an interesting application type mismatch saying essentially that the hba in le_antisymm hab hba has type b ≤ b

[Michael Stoll]

Previous discussion of rw at *.

[Thomas Murrills]

So, what's happening here is that the info trees (which determine what info is shown in the infoview) refer to metavariables created when elaborating le_antisymm _ _. However, when we use at *, internally we run tryTactic (which is just a try ... catch that returns true or false depending on success) on each available location. (We don't run tryTactic in other cases!)

Running try ... catch in TacticM is dangerous, though, because if an error occurs (as it does here!) the state (which knows about all the mvars we've created during elaboration of le_anti_symm _ _) is rewound—but the info trees aren't! So now the infotrees refer to metavariables which no longer exist in the current context, and we get the error above.

There are two solutions to this: either (1) rewind the infotrees on error as well, or (2) save the mvar context for the info trees (so that even if the tactic state no longer knows about these metavariables, the infotrees will, and we won't get an RPC error).

[Thomas Murrills]

My feeling is that try ... catch in TacticM/TermElabM simply ought to be safe with respect to infotrees, and save the infotree contexts on error. But I'm not sure if there are complications that make this tricky—and maybe there are arguments for rewinding the infotrees by default instead. Either way, it would be nice to not have to fiddle with infotrees on each try ... catch to simply avoid an RPC error! :)

[Thomas Murrills]

I've opened an issue about this: lean4#2965