fix: when pretty printing constant names, do not use aliases from "no…

…n-API `export`s" (#5689)

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.

Closes the already closed #2524

src/Lean/ResolveName.lean

@@ -398,16 +398,22 @@ Aliases are considered first.
 
 When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
 
+When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
+The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
+"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
+
 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
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
       | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
       | _ => return n₀ -- if can't resolve, return the original
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
+  unless allowHorizAliases do
+    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     if let some n ← unresolveNameCore initialName then

tests/lean/run/5689.lean

@@ -0,0 +1,17 @@
+/-!
+# Pretty printing shouldn't make use of "non-API exports"
+-/
+
+namespace A
+def n : Nat := 22
+end A
+
+namespace B
+export A (n)
+end B
+
+/-!
+Was `B.n`
+-/
+/-- info: A.n : Nat -/
+#guard_msgs in #check (A.n)

tests/lean/run/DVec.lean

@@ -41,7 +41,7 @@ example (v : Vec Nat 1) : Nat :=
 -- Does not work: Aliases find that `v` could be the `TypeVec` argument since `TypeVec` is an abbrev for `Vec`.
 /--
 error: application type mismatch
-  @Vec.hd ?_ v
+  @DVec.hd ?_ v
 argument
   v
 has type

tests/lean/run/alias.lean

@@ -26,7 +26,7 @@ However, this dot notation fails since there is no `FinSet` argument.
 However, unfolding is the preferred method.
 -/
 /--
-error: invalid field notation, function 'FinSet.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
+error: invalid field notation, function 'Set.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
 -/
 #guard_msgs in
 example (x y : FinSet 10) : FinSet 10 :=