From 094d11b472155567675999af41c779088f155516 Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Fri, 19 Nov 2021 14:20:44 +0100
Subject: [PATCH 1/3] fix: return fully-qualified name in PrettyPrinter when
 pp.fullNames is set

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 5 ++---
 tests/lean/236.lean.expected.out                 | 4 ++--
 tests/lean/eagerCoeExpansion.lean.expected.out   | 8 ++++----
 3 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index cb39f4c7e404..bea8360167e0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -59,9 +59,8 @@ def delabSort : Delab := do
 
 
 def unresolveNameGlobal (n₀ : Name) : DelabM Name := do
-  if n₀.hasMacroScopes then return n₀
-  let mut initialNames := #[]
-  if !(← getPPOption getPPFullNames) then initialNames := initialNames ++ getRevAliases (← getEnv) n₀
+  if n₀.hasMacroScopes || (← getPPOption getPPFullNames) then return n₀
+  let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     match (← unresolveNameCore initialName) with
diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out
index c655f84b7093..226d08e3ac5f 100644
--- a/tests/lean/236.lean.expected.out
+++ b/tests/lean/236.lean.expected.out
@@ -1,3 +1,3 @@
 { x := 10, b := true } : Foo
-Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) true : Foo
-{ x := OfNat.ofNat 10, b := true : Foo } : Foo
+Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
+{ x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo
diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out
index ab4180aa4240..df3395fe1244 100644
--- a/tests/lean/eagerCoeExpansion.lean.expected.out
+++ b/tests/lean/eagerCoeExpansion.lean.expected.out
@@ -8,18 +8,18 @@ fun (a : Nat) =>
     (@Eq.{1} Bool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      true)
+      Bool.true)
     (instDecidableEqBool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      true)
+      Bool.true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
-      true)
+      Bool.true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
-      true)
+      Bool.true)
 def s : Option Nat :=
 HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4

From 2cc7098c0d0cb4fd8c45079f79b3e77ffefcb3fb Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Fri, 19 Nov 2021 14:31:22 +0100
Subject: [PATCH 2/3] feat: show fully-qualified name in hover text

---
 src/Lean/Server/InfoUtils.lean                |  4 +-
 tests/lean/interactive/hoverDot.lean          |  1 +
 .../interactive/hoverDot.lean.expected.out    | 37 +++++++++++--------
 3 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 8a809a2c2e31..a1ff9a9b01b8 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki
 -/
 import Lean.DocString
 import Lean.Elab.InfoTree
+import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Util.Sorry
 
 protected structure String.Range where
@@ -164,7 +165,8 @@ where
     match i with
     | Info.ofTermInfo ti =>
       let tp ← Meta.inferType ti.expr
-      let eFmt ← Meta.ppExpr ti.expr
+      let eFmt ← Lean.withOptions (Lean.pp.fullNames.set . true) do
+        Meta.ppExpr ti.expr
       let tpFmt ← Meta.ppExpr tp
       -- try not to show too scary internals
       let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
diff --git a/tests/lean/interactive/hoverDot.lean b/tests/lean/interactive/hoverDot.lean
index 8b4b9cb0dde9..7d442d2a0c38 100644
--- a/tests/lean/interactive/hoverDot.lean
+++ b/tests/lean/interactive/hoverDot.lean
@@ -11,6 +11,7 @@ def Foo.foo : Foo := ⟨10⟩
 
 open Foo
 #check foo.f₁.succ
+     --^ textDocument/hover
          --^ textDocument/hover
             --^ textDocument/hover
 #check foo.f₂.succ
diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out
index 7adb2e511f96..58d5a0224e5c 100644
--- a/tests/lean/interactive/hoverDot.lean.expected.out
+++ b/tests/lean/interactive/hoverDot.lean.expected.out
@@ -3,11 +3,16 @@
 {"range":
  {"start": {"line": 8, "character": 7}, "end": {"line": 8, "character": 14}},
  "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hoverDot.lean"},
+ "position": {"line": 12, "character": 7}}
+{"range":
+ {"start": {"line": 12, "character": 7}, "end": {"line": 12, "character": 10}},
+ "contents": {"value": "```lean\nFoo.foo : Foo\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 12, "character": 11}}
 {"range":
  {"start": {"line": 12, "character": 11}, "end": {"line": 12, "character": 13}},
- "contents": {"value": "```lean\nf₁ : Foo → Nat\n```", "kind": "markdown"}}
+ "contents": {"value": "```lean\nFoo.f₁ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 12, "character": 14}}
 {"range":
@@ -15,35 +20,35 @@
  "contents":
  {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 15, "character": 11}}
+ "position": {"line": 16, "character": 11}}
 {"range":
- {"start": {"line": 15, "character": 11}, "end": {"line": 15, "character": 13}},
- "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
+ {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 13}},
+ "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 15, "character": 14}}
+ "position": {"line": 16, "character": 14}}
 {"range":
- {"start": {"line": 15, "character": 14}, "end": {"line": 15, "character": 18}},
+ {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}},
  "contents":
  {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 18, "character": 13}}
+ "position": {"line": 19, "character": 13}}
 {"range":
- {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 15}},
- "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
+ {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 15}},
+ "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 18, "character": 16}}
+ "position": {"line": 19, "character": 16}}
 {"range":
- {"start": {"line": 18, "character": 16}, "end": {"line": 18, "character": 20}},
+ {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}},
  "contents":
  {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 21, "character": 14}}
+ "position": {"line": 22, "character": 14}}
 {"range":
- {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 16}},
- "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
+ {"start": {"line": 22, "character": 14}, "end": {"line": 22, "character": 16}},
+ "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
- "position": {"line": 21, "character": 17}}
+ "position": {"line": 22, "character": 17}}
 {"range":
- {"start": {"line": 21, "character": 17}, "end": {"line": 21, "character": 21}},
+ {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}},
  "contents":
  {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}

From 5c4ac8ad5fd268b11121250ec849c71b11947d8c Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Sun, 21 Nov 2021 15:04:10 +0100
Subject: [PATCH 3/3] fix: handle _root_ in unresolveNameGlobal with
 pp.fullNames

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean |  6 +++++-
 tests/lean/interactive/hover.lean                | 13 +++++++++++++
 tests/lean/interactive/hover.lean.expected.out   | 12 ++++++++++++
 3 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index bea8360167e0..7d5fcda18b54 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -59,7 +59,11 @@ def delabSort : Delab := do
 
 
 def unresolveNameGlobal (n₀ : Name) : DelabM Name := do
-  if n₀.hasMacroScopes || (← getPPOption getPPFullNames) then return n₀
+  if n₀.hasMacroScopes then return n₀
+  if (← getPPOption getPPFullNames) then
+    match (← resolveGlobalName n₀) with
+      | [(potentialMatch, _)] => if 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
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 8f248e70af68..f98092e5fa35 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -101,3 +101,16 @@ example : Id Nat := do
   n := 2
 --^ textDocument/hover
   n
+
+
+constant foo : Nat
+
+#check _root_.foo
+       --^ textDocument/hover
+
+namespace Bar
+
+constant foo : Nat
+
+#check _root_.foo
+       --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 4ef5415a1616..d0941a945b01 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -91,3 +91,15 @@ null
 {"range":
  {"start": {"line": 100, "character": 2}, "end": {"line": 100, "character": 3}},
  "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 107, "character": 9}}
+{"range":
+ {"start": {"line": 107, "character": 7},
+  "end": {"line": 107, "character": 17}},
+ "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 114, "character": 9}}
+{"range":
+ {"start": {"line": 114, "character": 7},
+  "end": {"line": 114, "character": 17}},
+ "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}}