From ced8df3e860721324cf8f36832e13f7b84b13edd Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Mon, 4 Jul 2022 19:49:05 +0200
Subject: [PATCH] fix: references of variables with equal ranges

---
 src/Lean/Linter/Basic.lean                    |  2 +-
 src/Lean/Server/References.lean               | 28 ++++++++++---------
 .../interactive/highlight.lean.expected.out   | 12 ++++----
 tests/lean/linterUnusedVariables.lean         |  8 ++++++
 .../linterUnusedVariables.lean.expected.out   | 11 ++++----
 5 files changed, 36 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index dc627c584d..2a25bd2b7c 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -40,7 +40,7 @@ def unusedVariables : Linter := fun stx => do
     return
 
   -- collect references
-  let refs := findModuleRefs fileMap infoTrees
+  let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true)
 
   let mut vars : HashMap FVarId RefInfo := .empty
   let mut constDecls : HashSet String.Range := .empty
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index dc48abf3f6..d3b86b3395 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -178,13 +178,11 @@ partial def combineFvars (refs : Array Reference) : Array Reference := Id.run do
   let mut refs' := #[]
   for ref in refs do
     match ref with
-    | { ident := ident@(RefIdent.fvar id), isBinder, .. } =>
-      if isBinder && idMap.contains id then
-        -- downgrade chained definitions to usages
-        -- (we shouldn't completely remove them in case they do not have usages)
-        refs' := refs'.push { ref with ident := applyIdMap idMap ident, isBinder := false, aliases := #[ident] }
-      else
-        refs' := refs'.push { ref with ident := applyIdMap idMap ident }
+    | { ident := ident@(RefIdent.fvar id), .. } =>
+      if idMap.contains id then
+        refs' := refs'.push { ref with ident := applyIdMap idMap ident, aliases := #[ident] }
+      else if !idMap.contains id then
+        refs' := refs'.push ref
     | _ =>
       refs' := refs'.push ref
   refs'
@@ -198,20 +196,24 @@ where
     | m, RefIdent.fvar id => RefIdent.fvar <| findCanonicalBinder m id
     | _, ident => ident
 
-def dedupReferences (refs : Array Reference) : Array Reference := Id.run do
-  let mut refsByIdAndRange : HashMap (RefIdent × Lsp.Range) Reference := HashMap.empty
+def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := false) : Array Reference := Id.run do
+  let mut refsByIdAndRange : HashMap (RefIdent × Option Bool × Lsp.Range) Reference := HashMap.empty
   for ref in refs do
-    let key := (ref.ident, ref.range)
+    let isBinder := if allowSimultaneousBinderUse then some ref.isBinder else none
+    let key := (ref.ident, isBinder, ref.range)
     refsByIdAndRange := match refsByIdAndRange[key] with
-      | some ref' => refsByIdAndRange.insert key { ref' with isBinder := ref'.isBinder || ref.isBinder, aliases := ref'.aliases ++ ref.aliases }
+      | some ref' => refsByIdAndRange.insert key { ref' with aliases := ref'.aliases ++ ref.aliases }
       | none => refsByIdAndRange.insert key ref
 
   let dedupedRefs := refsByIdAndRange.fold (init := #[]) fun refs _ ref => refs.push ref
   return dedupedRefs.qsort (·.range < ·.range)
 
 def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool := true)
-    : ModuleRefs := Id.run do
-  let mut refs := dedupReferences <| combineFvars <| findReferences text trees
+    (allowSimultaneousBinderUse := false) : ModuleRefs := Id.run do
+  let mut refs :=
+    dedupReferences (allowSimultaneousBinderUse := allowSimultaneousBinderUse) <|
+    combineFvars <|
+    findReferences text trees
   if !localVars then
     refs := refs.filter fun
       | { ident := RefIdent.fvar _, .. } => false
diff --git a/tests/lean/interactive/highlight.lean.expected.out b/tests/lean/interactive/highlight.lean.expected.out
index 10c86ad5a6..8feb7444c4 100644
--- a/tests/lean/interactive/highlight.lean.expected.out
+++ b/tests/lean/interactive/highlight.lean.expected.out
@@ -82,9 +82,6 @@
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 41, "character": 7}}
 [{"range":
-  {"start": {"line": 38, "character": 4}, "end": {"line": 38, "character": 5}},
-  "kind": 1},
- {"range":
   {"start": {"line": 34, "character": 10},
    "end": {"line": 34, "character": 11}},
   "kind": 1},
@@ -94,6 +91,9 @@
  {"range":
   {"start": {"line": 36, "character": 9}, "end": {"line": 36, "character": 10}},
   "kind": 1},
+ {"range":
+  {"start": {"line": 38, "character": 4}, "end": {"line": 38, "character": 5}},
+  "kind": 1},
  {"range":
   {"start": {"line": 38, "character": 9}, "end": {"line": 38, "character": 10}},
   "kind": 1},
@@ -107,12 +107,12 @@
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 48, "character": 9}}
 [{"range":
-  {"start": {"line": 47, "character": 4}, "end": {"line": 47, "character": 5}},
-  "kind": 1},
- {"range":
   {"start": {"line": 45, "character": 10},
    "end": {"line": 45, "character": 11}},
   "kind": 1},
+ {"range":
+  {"start": {"line": 47, "character": 4}, "end": {"line": 47, "character": 5}},
+  "kind": 1},
  {"range":
   {"start": {"line": 48, "character": 9}, "end": {"line": 48, "character": 10}},
   "kind": 1}]
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index 794397d86e..979dc080e9 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -205,6 +205,14 @@ opaque externConst (x : Nat) : Nat :=
   let y := 3
   5
 
+
+macro "useArg " name:declId arg:ident : command => `(def $name ($arg : α) : α := $arg)
+useArg usedMacroVariable a
+
+macro "doNotUseArg " name:declId arg:ident : command => `(def $name ($arg : α) : Nat := 3)
+doNotUseArg unusedMacroVariable b
+
+
 theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by -- *not* unused
   cases a
   exact absurd h (Nat.not_lt_zero _)
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index ed5a73ce10..ce2bfb3bbb 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -26,7 +26,8 @@ linterUnusedVariables.lean:191:19-191:20: warning: unused variable `x`
 linterUnusedVariables.lean:195:6-195:7: warning: unused variable `y`
 linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
 linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
-linterUnusedVariables.lean:214:27-214:28: error: don't know how to synthesize placeholder
+linterUnusedVariables.lean:213:32-213:33: warning: unused variable `b`
+linterUnusedVariables.lean:222:27-222:28: error: don't know how to synthesize placeholder
 context:
 bar : ?m
 bar' : Nat → Nat
@@ -35,10 +36,10 @@ bar' : Nat → Nat
 inst : ToString α
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:215:0-215:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:216:0-216:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:219:0: error: expected '{' or tactic
-linterUnusedVariables.lean:217:27-217:29: error: unsolved goals
+linterUnusedVariables.lean:223:0-223:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:224:0-224:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:227:0: error: expected '{' or tactic
+linterUnusedVariables.lean:225:27-225:29: error: unsolved goals
 bar : ?m
 bar' : Nat → Nat
 α : Type ?u