From f4fbf923136dd768cd277c1fe5be173161bd24d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Sep 2022 16:21:24 -0700
Subject: [PATCH] fix: make `privateToUserNameAux` more robust

---
 src/Lean/Modifiers.lean                       | 23 ++++++++++++++++---
 tests/lean/prvNameWithMacroScopes.lean        |  2 ++
 .../prvNameWithMacroScopes.lean.expected.out  |  2 ++
 3 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/prvNameWithMacroScopes.lean
 create mode 100644 tests/lean/prvNameWithMacroScopes.lean.expected.out

diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean
index 3048be1280..710cc3d65e 100644
--- a/src/Lean/Modifiers.lean
+++ b/src/Lean/Modifiers.lean
@@ -42,9 +42,26 @@ def isPrivateName : Name → Bool
 def isPrivateNameExport (n : Name) : Bool :=
   isPrivateName n
 
-private def privateToUserNameAux : Name → Name
-  | .str p s => Name.mkStr (privateToUserNameAux p) s
-  | _        => Name.anonymous
+/--
+Return `true` if `n` is of the form `_private.<module_name>.0`
+See comment above.
+-/
+private def isPrivatePrefix (n : Name) : Bool :=
+  match n with
+  | .num p 0 => go p
+  | _ => false
+where
+  go (n : Name) : Bool :=
+    n == privateHeader ||
+    match n with
+    | .str p _ => go p
+    | _ => false
+
+private def privateToUserNameAux (n : Name) : Name :=
+  match n with
+  | .str p s => .str (privateToUserNameAux p) s
+  | .num p i => if isPrivatePrefix n then .anonymous else .num (privateToUserNameAux p) i
+  | _        => .anonymous
 
 @[export lean_private_to_user_name]
 def privateToUserName? (n : Name) : Option Name :=
diff --git a/tests/lean/prvNameWithMacroScopes.lean b/tests/lean/prvNameWithMacroScopes.lean
new file mode 100644
index 0000000000..cd97591112
--- /dev/null
+++ b/tests/lean/prvNameWithMacroScopes.lean
@@ -0,0 +1,2 @@
+import Lean
+#print Lean.instBEqFVarId
diff --git a/tests/lean/prvNameWithMacroScopes.lean.expected.out b/tests/lean/prvNameWithMacroScopes.lean.expected.out
new file mode 100644
index 0000000000..b19042cbc9
--- /dev/null
+++ b/tests/lean/prvNameWithMacroScopes.lean.expected.out
@@ -0,0 +1,2 @@
+def Lean.instBEqFVarId : BEq Lean.FVarId :=
+{ beq := Lean.beqFVarId✝ }