fix: connect occurrences of mutable variable inside and outside for in info tree

src/Lean/Elab/Do.lean

@@ -1245,10 +1245,6 @@ def tryCatchPred (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : O
   | none => false
   | some finallyCode => p finallyCode.code
 
-def mutVarNamesToDefStx (mutVars : Array Syntax) : M (Array Syntax) := do
-  let ctx ← read
-  return mutVars.map fun v => ctx.mutableVars.findD v.getId v
-
 mutual
   /- "Concatenate" `c` with `doSeqToCode doElems` -/
   partial def concatWith (c : CodeBlock) (doElems : List Syntax) : M CodeBlock :=
@@ -1423,6 +1419,11 @@ mutual
       let forElems  := getDoSeqElems doFor[3]
       let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
       let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
+      let ctx ← read
+      -- semantic no-op that replaces the `uvars`' position information (which all point inside the loop)
+      -- with that of the respective mutable declarations outside the loop, which allows the language
+      -- server to identify them as conceptually identical variables
+      let uvars := uvars.map fun v => ctx.mutableVars.findD v.getId v
       let uvarsTuple ← liftMacroM do mkTuple uvars
       if hasReturn forInBodyCodeBlock.code then
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody

tests/lean/interactive/highlight.lean

@@ -1,5 +1,5 @@
 
-def foo1(bar : Nat) : Nat := 3
+def foo1(bar : Nat) : Bool := true
                      --^ textDocument/documentHighlight
 
 #eval foo1 2
@@ -30,3 +30,14 @@ example : Nat := Id.run do
   x := 2
   x
 --^ textDocument/documentHighlight
+
+example : Nat := Id.run do
+  let mut y : Nat := 0
+  for x in [0] do
+    y := y + x
+  if true then
+    y := y + 1
+  else
+    return y
+  pure y
+     --^ textDocument/documentHighlight

tests/lean/interactive/highlight.lean.expected.out

@@ -1,31 +1,7 @@
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 1, "character": 23}}
 [{"range":
-  {"start": {"line": 1, "character": 15}, "end": {"line": 1, "character": 18}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 1, "character": 22}, "end": {"line": 1, "character": 25}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 8, "character": 11}, "end": {"line": 8, "character": 14}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 14, "character": 8}, "end": {"line": 14, "character": 11}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 15, "character": 9}, "end": {"line": 15, "character": 12}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 18, "character": 23},
-   "end": {"line": 18, "character": 26}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 22, "character": 16},
-   "end": {"line": 22, "character": 19}},
-  "kind": 1},
- {"range":
-  {"start": {"line": 27, "character": 10},
-   "end": {"line": 27, "character": 13}},
+  {"start": {"line": 1, "character": 22}, "end": {"line": 1, "character": 26}},
   "kind": 1}]
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 5, "character": 7}}
@@ -103,3 +79,28 @@
  {"range":
   {"start": {"line": 30, "character": 2}, "end": {"line": 30, "character": 3}},
   "kind": 1}]
+{"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},
+ {"range":
+  {"start": {"line": 36, "character": 4}, "end": {"line": 36, "character": 5}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 36, "character": 9}, "end": {"line": 36, "character": 10}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 38, "character": 9}, "end": {"line": 38, "character": 10}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 40, "character": 11},
+   "end": {"line": 40, "character": 12}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 41, "character": 7}, "end": {"line": 41, "character": 8}},
+  "kind": 1}]