hygiene issues in macros with repeated names

Stream: lean4

[Eric Wieser]

I'm struggling a little with this example:

syntax "apply_mt" (ppSpace colGt ident (" with " ident)?) : tactic
macro_rules
  | `(tactic| apply_mt $e with $e') => `(tactic|
    refine mt (fun $e' => ?_) $e; clear $e)

theorem ok {a b c d : Nat} (h : a ≠ b) : c ≠ d := by
  apply_mt h with h1
  -- h1 : c = d ⊢ a = b
  sorry

theorem bad {a b c d : Nat} (h : a ≠ b) : c ≠ d := by
  apply_mt h with h
  -- h1 : a ≠ b ⊢ a = b
  sorry

Here, the first tactic works as intended, but the second fails due to aliasing between the $e and $e' macro arguments. Is there a recommended workaround for this?

[Eric Wieser]

Ideally I'd have some way to resolve the name up front; but presumably I can only do that within a elab_rules not a macro_rules?

[Eric Wieser]

(I know here that I can just rewrite the tactic to use intro rather than fun to resolve the issue, but I was hoping for a more general solution)