fix: references of variables with equal ranges

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

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

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}]

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 _)

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