fix: avoid new term info around def bodies (#6031)

This PR fixes a regression with go-to-definition and document highlight
misbehaving on tactic blocks.

We explicitly avoid creating term info nodes around `by` blocks, which
#5338 might accidentally do; as the new info is not relevant for the
server, it is instead moved into a custom info.

Reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Go-to-def.20for.20tactics.20broken.20on.20v4.2E14.2E0-rc1.

src/Lean/Elab/LetRec.lean

@@ -90,9 +90,9 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx (mkInfo := mkTermInfo `MutualDef.body view.valStx) do
-         let value ← elabTermEnsuringType view.valStx type
-         mkLambdaFVars xs value
+        withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
+          let value ← elabTermEnsuringType view.valStx type
+          mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

src/Lean/Elab/MutualDef.lean

@@ -417,7 +417,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again
-          withInfoContext' valStx (mkInfo := mkTermInfo `MutualDef.body valStx) do
+          withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
             -- synthesize mvars here to force the top-level tactic block (if any) to run
             let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
             -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that

src/Lean/Elab/Term.lean

@@ -1339,6 +1339,21 @@ def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → Term
   else
     Elab.withInfoContext' x mkInfo
 
+/-- Info node capturing `def/let rec` bodies, used by the unused variables linter. -/
+structure BodyInfo where
+  /-- The body as a fully elaborated term. -/
+  value : Expr
+deriving TypeName
+
+/-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`. -/
+def mkBodyInfo (stx : Syntax) (value : Expr) : Info :=
+  .ofCustomInfo { stx, value := .mk { value : BodyInfo } }
+
+/-- Extracts a `BodyInfo` custom info. -/
+def getBodyInfo? : Info → Option BodyInfo
+  | .ofCustomInfo { value, .. } => value.get? BodyInfo
+  | _ => none
+
 /--
 Postpone the elaboration of `stx`, return a metavariable that acts as a placeholder, and
 ensures the info tree is updated and a hole id is introduced.

src/Lean/Linter/UnusedVariables.lean

@@ -18,7 +18,7 @@ It is not immediately obvious but this is a surprisingly expensive check without
 some optimizations.  The main complication is that it can be difficult to
 determine what constitutes a "use" apart from direct references to a variable
 that we can easily find in the info tree.  For example, we would like this to be
-considered a use of `x`: 
+considered a use of `x`:
 ```
 def foo (x : Nat) : Nat := by assumption
 ```
@@ -390,22 +390,20 @@ where
         -- set if `analyzeTactics` is unset, tactic infos are present, and we're inside the body
         let ignored ← read
         match info with
+        | .ofCustomInfo ti =>
+          if !linter.unusedVariables.analyzeTactics.get ci.options then
+            if let some bodyInfo := ti.value.get? Elab.Term.BodyInfo then
+              -- the body is the only `Expr` we will analyze in this case
+              -- NOTE: we include it even if no tactics are present as at least for parameters we want
+              -- to lint only truly unused binders
+              let (e, _) := instantiateMVarsCore ci.mctx bodyInfo.value
+              modify fun s => { s with
+                assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+              let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+              withReader (· || tacticsPresent) do
+                go children.toArray ci
+              return false
         | .ofTermInfo ti =>
-          -- NOTE: we have to do this check *before* `ignored` because nested bodies (e.g. from
-          -- nested `let rec`s) do need to be included to find all `Expr` uses of the top-level
-          -- parameters
-          if ti.elaborator == `MutualDef.body &&
-              !linter.unusedVariables.analyzeTactics.get ci.options then
-            -- the body is the only `Expr` we will analyze in this case
-            -- NOTE: we include it even if no tactics are present as at least for parameters we want
-            -- to lint only truly unused binders
-            let (e, _) := instantiateMVarsCore ci.mctx ti.expr
-            modify fun s => { s with
-              assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
-            let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
-            withReader (· || tacticsPresent) do
-              go children.toArray ci
-            return false
           if ignored then return true
           match ti.expr with
           | .const .. =>
@@ -441,22 +439,20 @@ where
               -- Found a direct use, keep track of it
               modify fun s => { s with fvarUses := s.fvarUses.insert id }
           | _ => pure ()
-          return true
         | .ofTacticInfo ti =>
           -- When ignoring new binders, no need to look at intermediate tactic states either as
           -- references to binders outside the body will be covered by the body `Expr`
           if ignored then return true
           -- Keep track of the `MetavarContext` after a tactic for later
           modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
-          return true
         | .ofFVarAliasInfo i =>
           if ignored then return true
           -- record any aliases we find
           modify fun s =>
             let id := followAliases s.fvarAliases i.baseId
             { s with fvarAliases := s.fvarAliases.insert i.id id }
-          return true
-        | _ => return true)
+        | _ => pure ()
+        return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -29,9 +29,7 @@ a : α
       • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
       • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
       • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-      • match α, β, x, a with
-        | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
-        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ MutualDef.body
+      • CustomInfo(Lean.Elab.Term.BodyInfo)
         • match α, β, x, a with
           | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
           | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch

tests/lean/interactive/highlight.lean

@@ -54,3 +54,11 @@ example (x : Option Nat) : Nat :=
   | some x => 1
        --^ textDocument/documentHighlight
   | none   => 0
+
+/-!
+A helper term info node accidentally led to this highlight including `by` (and "go to definition"
+jumping to `rfl` in full projects).
+-/
+example : True := by
+  simp
+--^ textDocument/documentHighlight

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

@@ -121,3 +121,6 @@
 [{"range":
   {"start": {"line": 53, "character": 9}, "end": {"line": 53, "character": 10}},
   "kind": 1}]
+{"textDocument": {"uri": "file:///highlight.lean"},
+ "position": {"line": 62, "character": 2}}
+[]