fix: rename_i in macro

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -352,12 +352,21 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
     let mut info  := #[]
     let mut found : NameSet := {}
     let n := lctx.numIndices
+    -- hypotheses are inaccessible if their scopes are different from the caller's (we assume that
+    -- the scopes are the same for all the hypotheses in `hs`, which is reasonable to expect in
+    -- practice and otherwise the expected semantics of `rename_i` really are not clear)
+    let some callerScopes := hs.findSome? (fun
+        | `(binderIdent| $h:ident) => some <| extractMacroScopes h.getId
+        | _ => none)
+      | return mvarId
     for i in [:n] do
       let j := n - i - 1
       match lctx.getAt? j with
       | none => pure ()
       | some localDecl =>
-        if localDecl.userName.hasMacroScopes || found.contains localDecl.userName then
+        let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
+        let shadowed := found.contains localDecl.userName
+        if inaccessible || shadowed then
           if let `(binderIdent| $h:ident) := hs.back then
             let newName := h.getId
             lctx := lctx.setUserName localDecl.fvarId newName

src/Lean/Elab/Util.lean

@@ -24,6 +24,13 @@ def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format
     else
       view.scopes.foldl Name.mkNum (view.name ++ view.imported ++ view.mainModule)
 
+/--
+Two names are from the same lexical scope if their scoping information modulo `MacroScopesView.name`
+is equal.
+-/
+def MacroScopesView.equalScope (a b : MacroScopesView) : Bool :=
+  a.scopes == b.scopes && a.mainModule == b.mainModule && a.imported == b.imported
+
 namespace Elab
 
 def expandOptNamedPrio (stx : Syntax) : MacroM Nat :=

tests/lean/run/renameI.lean

@@ -5,3 +5,19 @@ example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by
   apply Eq.symm
   exact h2
   exact h1
+
+/-!
+Within a tactic macro, all identifiers *not* from this quotation should be regarded as inaccessible.
+-/
+
+macro "my_tac " h:ident : tactic =>
+ `(tactic| (
+   cases $h:ident
+   rename_i h_p3
+   rename_i h_p1_p2 -- must rename `left`, not `h_p3`
+   cases h_p1_p2  -- fails otherwise
+   ))
+
+example (h : (p1 ∧ p2) ∧ p3) : True := by
+  my_tac h
+  sorry