From a1be9ec8505544801583a41fa3ac1640491958fa Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 10 May 2024 15:37:34 -0700
Subject: [PATCH] chore: tidying up `Lean.unresolveNameGlobal` (#4091)

The main loop logic could be simplified, and `if let` could be used to
make control flow more obvious.

Also adds a check for macro scopes to prevent `unresolveNameGlobal` from
returning names with macro scopes in the event there's an alias with
one.

This is a follow up to #3946.
---
 src/Lean/ResolveName.lean | 28 ++++++++++++++++++----------
 tests/lean/run/2291.lean  | 22 ++++++++++++++++++++++
 2 files changed, 40 insertions(+), 10 deletions(-)

diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 91bef0d99b6e..6c583629b3ae 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -384,6 +384,16 @@ After `open Foo open Boo`, we have
 def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
   ensureNonAmbiguous id (← resolveGlobalConst id)
 
+/--
+Finds a name that unambiguously resolves to the given name `n₀`.
+Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
+Aliases are considered first.
+
+When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
+
+This function is meant to be used for pretty printing.
+If `n₀` is an accessible name, then the result will be an accessible name.
+-/
 def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
@@ -393,21 +403,19 @@ def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
-    match (← unresolveNameCore initialName) with
-    | none => continue
-    | some n => return n
+    if let some n ← unresolveNameCore initialName then
+      return n
   return n₀ -- if can't resolve, return the original
 where
   unresolveNameCore (n : Name) : m (Option Name) := do
+    if n.hasMacroScopes then return none
     let mut revComponents := n.componentsRev
     let mut candidate := Name.anonymous
-    for _ in [:revComponents.length] do
-      match revComponents with
-      | [] => return none
-      | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest
-      match (← resolveGlobalName candidate) with
-      | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
-      | _ => continue
+    for cmpt in revComponents do
+      candidate := Name.appendCore cmpt candidate
+      if let [(potentialMatch, _)] ← resolveGlobalName candidate then
+        if potentialMatch == n₀ then
+          return some candidate
     return none
 
 end Lean
diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean
index 0390315bd03c..d7791536e01b 100644
--- a/tests/lean/run/2291.lean
+++ b/tests/lean/run/2291.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.Command
+import Lean.Elab.Open
 /-!
 Issue #2291
 
@@ -6,3 +8,23 @@ The following example would cause the pretty printer to panic.
 
 set_option trace.compiler.simp true in
 #eval [0]
+
+
+/-!
+Fixing the above involved changing `Lean.unresolveNameGlobal`.
+Here, we also verify that we do not pretty print using any aliases that have macro scopes.
+-/
+
+open Lean in
+elab "add_bad_alias " n:ident : command => withFreshMacroScope do
+  let declName ← Elab.OpenDecl.resolveNameUsingNamespaces [← getCurrNamespace] n
+  let badName ← MonadQuotation.addMacroScope `bad
+  modify fun s => { s with env := addAlias s.env badName declName }
+
+def f := 1
+
+add_bad_alias f
+
+-- Formerly was info: bad✝ : ℕ
+/-- info: f : Nat -/
+#guard_msgs in #check (f)