From a9db0d2e535752e316532be8ecdcc9cce90927ef Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 24 Apr 2024 08:07:18 -0700
Subject: [PATCH] fix: use `Name.appendCore` instead of `Name.append` in
 `unresolveNameGlobal` (#3946)

`Name.append` has special handling of macro scopes, and it would cause
`unresolveNameGlobal` to panic. Using `Name.appendCore` to append name
parts is justified by the fact that it's being used to reassemble a
disassembled name.

Closes #2291
---
 src/Init/Prelude.lean     | 9 +++++++--
 src/Lean/ResolveName.lean | 2 +-
 tests/lean/run/2291.lean  | 8 ++++++++
 3 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/2291.lean

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 8d3354fc03..e9bc2632ac 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -4335,8 +4335,13 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 /--
-Append two names that may have macro scopes. The macro scopes in `b` are always erased.
-If `a` has macro scopes, then they are propagated to the result of `append a b`.
+Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
+Panics if both `a` and `b` have macro scopes.
+
+This function is used for the `Append Name` instance.
+
+See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes.
+Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.
 -/
 def Name.append (a b : Name) : Name :=
   match a.hasMacroScopes, b.hasMacroScopes with
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 34c800fb48..91bef0d99b 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -404,7 +404,7 @@ where
     for _ in [:revComponents.length] do
       match revComponents with
       | [] => return none
-      | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest
+      | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest
       match (← resolveGlobalName candidate) with
       | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
       | _ => continue
diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean
new file mode 100644
index 0000000000..0390315bd0
--- /dev/null
+++ b/tests/lean/run/2291.lean
@@ -0,0 +1,8 @@
+/-!
+Issue #2291
+
+The following example would cause the pretty printer to panic.
+-/
+
+set_option trace.compiler.simp true in
+#eval [0]