fix: jump to definition for recursive declarations

src/Lean/Elab/MutualDef.lean

@@ -729,6 +729,8 @@ where
     let headers ← levelMVarToParamHeaders views headers
     let allUserLevelNames := getAllUserLevelNames headers
     withFunLocalDecls headers fun funFVars => do
+      for header in headers, funFVar in funFVars do
+        addTermInfo (isBinder := true) header.ref funFVar
       let values ← elabFunValues headers
       Term.synthesizeSyntheticMVarsNoPostponing
       let values ← values.mapM (instantiateMVars ·)

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

@@ -22,6 +22,7 @@ a : α
   x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
   β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
     β : Type @ ⟨7, 33⟩-⟨7, 34⟩
+  _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨10, 19⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
   _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>

tests/lean/infoTree.lean.expected.out

@@ -16,6 +16,7 @@
         Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
           [.] `Nat : some Type.{?_uniq.425} @ ⟨13, 24⟩-⟨13, 27⟩
           Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
+  f (isBinder := true) : Nat → Nat × Nat @ ⟨13, 0⟩-⟨15, 6⟩
   x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
   let y := (x, x);
   id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl
@@ -70,6 +71,7 @@
                   0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit
             x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
               x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
+  h (isBinder := true) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨17, 0⟩-⟨19, 8⟩
   fun x y b =>
     of_eq_true
       (Eq.trans (congrFun (congrArg Eq (Nat.add_zero x)) x)
@@ -127,6 +129,7 @@
       Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
         [.] `Nat : some Sort.{?_uniq.586} @ ⟨21, 36⟩-⟨21, 39⟩
         Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
+  f2 (isBinder := true) : Nat → Nat → Bool → Nat @ ⟨21, 0⟩-⟨25, 10⟩
   fun x y b =>
     let _discr := (x + y, x - y);
     match (x + y, x - y) with
@@ -275,6 +278,7 @@
     Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
       [.] `Nat : some Type.{?_uniq.802} @ ⟨27, 45⟩-⟨27, 48⟩
       Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
+  f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 0⟩-⟨28, 17⟩
   s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
   Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
     s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@@ -295,6 +299,7 @@
   Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
     [.] `Nat : some Sort.{?_uniq.846} @ ⟨30, 19⟩-⟨30, 22⟩
     Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
+  f4 (isBinder := true) : B → Nat @ ⟨30, 0⟩-⟨31, 20⟩
   arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
   A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
     arg : B @ ⟨31, 2⟩-⟨31, 5⟩
@@ -314,6 +319,7 @@
   B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
     [.] `B : some Sort.{?_uniq.869} @ ⟨33, 19⟩-⟨33, 20⟩
     B : Type @ ⟨33, 19⟩-⟨33, 20⟩
+  f5 (isBinder := true) : Nat → B @ ⟨33, 0⟩-⟨35, 1⟩
   x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
   { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
     ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen
@@ -369,6 +375,7 @@ infoTree.lean:44:0: error: expected stx
           _uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
         _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
           _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
+  _uniq.898 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 0⟩-⟨47, 8⟩
   _uniq.901 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
   _uniq.902 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
   (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.901 _uniq.902]) f6.f7 : Eq.{1} Nat _uniq.901 _uniq.901 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
@@ -414,6 +421,7 @@ infoTree.lean:44:0: error: expected stx
   B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
     [.] `B : some Sort.{?_uniq.941} @ ⟨50, 17⟩-⟨50, 18⟩
     B : Type @ ⟨50, 17⟩-⟨50, 18⟩
+  _uniq.942 (isBinder := true) : B -> B @ ⟨50, 0⟩-⟨50, 32⟩
   _uniq.944 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
   B.mk (B.pair _uniq.944) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
     B.pair _uniq.944 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj

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

@@ -22,6 +22,9 @@
  {"range":
   {"start": {"line": 22, "character": 16},
    "end": {"line": 22, "character": 19}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 30}},
   "kind": 1}]
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 5, "character": 7}}
@@ -37,6 +40,9 @@
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 10, "character": 3}}
 [{"range":
+  {"start": {"line": 8, "character": 0}, "end": {"line": 10, "character": 9}},
+  "kind": 1},
+ {"range":
   {"start": {"line": 9, "character": 6}, "end": {"line": 9, "character": 9}},
   "kind": 1},
  {"range":
@@ -61,6 +67,9 @@
   "kind": 1},
  {"range":
   {"start": {"line": 23, "character": 4}, "end": {"line": 23, "character": 7}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 18, "character": 0}, "end": {"line": 19, "character": 9}},
   "kind": 1}]
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 23, "character": 5}}
@@ -72,6 +81,9 @@
   "kind": 1},
  {"range":
   {"start": {"line": 23, "character": 4}, "end": {"line": 23, "character": 7}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 22, "character": 0}, "end": {"line": 23, "character": 29}},
   "kind": 1}]
 {"textDocument": {"uri": "file://highlight.lean"},
  "position": {"line": 23, "character": 12}}
@@ -86,4 +98,7 @@
  {"range":
   {"start": {"line": 23, "character": 24},
    "end": {"line": 23, "character": 27}},
+  "kind": 1},
+ {"range":
+  {"start": {"line": 22, "character": 0}, "end": {"line": 23, "character": 29}},
   "kind": 1}]

tests/lean/interactive/jumpMutual.lean

@@ -0,0 +1,24 @@
+mutual
+
+def h (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+               --v textDocument/definition
+  | x+1 => f x + r x
+         --^ textDocument/definition
+where
+  r : Nat → Nat
+  | 0 => 1
+           --v textDocument/definition
+  | x + 1 => r x * h x
+                 --^ textDocument/definition
+
+def f (x : Nat) : Nat :=
+  let rec g : Nat → Nat
+    | 0 => 1
+               --v textDocument/definition
+    | n+1 => 2 * g n
+--v textDocument/definition
+  g x + h x
+      --^ textDocument/definition
+end

tests/lean/interactive/jumpMutual.lean.expected.out

@@ -0,0 +1,70 @@
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 6, "character": 17}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 9, "character": 2}, "end": {"line": 9, "character": 3}},
+  "targetRange":
+  {"start": {"line": 9, "character": 2}, "end": {"line": 9, "character": 3}},
+  "originSelectionRange":
+  {"start": {"line": 6, "character": 17}, "end": {"line": 6, "character": 18}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 6, "character": 11}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 15, "character": 0}, "end": {"line": 21, "character": 11}},
+  "targetRange":
+  {"start": {"line": 15, "character": 0}, "end": {"line": 21, "character": 11}},
+  "originSelectionRange":
+  {"start": {"line": 6, "character": 11}, "end": {"line": 6, "character": 12}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 12, "character": 13}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 9, "character": 2}, "end": {"line": 9, "character": 3}},
+  "targetRange":
+  {"start": {"line": 9, "character": 2}, "end": {"line": 9, "character": 3}},
+  "originSelectionRange":
+  {"start": {"line": 12, "character": 13},
+   "end": {"line": 12, "character": 14}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 12, "character": 19}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 2, "character": 0}, "end": {"line": 12, "character": 22}},
+  "targetRange":
+  {"start": {"line": 2, "character": 0}, "end": {"line": 12, "character": 22}},
+  "originSelectionRange":
+  {"start": {"line": 12, "character": 19},
+   "end": {"line": 12, "character": 20}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 19, "character": 17}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 16, "character": 10},
+   "end": {"line": 16, "character": 11}},
+  "targetRange":
+  {"start": {"line": 16, "character": 10},
+   "end": {"line": 16, "character": 11}},
+  "originSelectionRange":
+  {"start": {"line": 19, "character": 17},
+   "end": {"line": 19, "character": 18}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 21, "character": 2}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 16, "character": 10},
+   "end": {"line": 16, "character": 11}},
+  "targetRange":
+  {"start": {"line": 16, "character": 10},
+   "end": {"line": 16, "character": 11}},
+  "originSelectionRange":
+  {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 3}}}]
+{"textDocument": {"uri": "file://jumpMutual.lean"},
+ "position": {"line": 21, "character": 8}}
+[{"targetUri": "file://jumpMutual.lean",
+  "targetSelectionRange":
+  {"start": {"line": 2, "character": 0}, "end": {"line": 12, "character": 22}},
+  "targetRange":
+  {"start": {"line": 2, "character": 0}, "end": {"line": 12, "character": 22}},
+  "originSelectionRange":
+  {"start": {"line": 21, "character": 8}, "end": {"line": 21, "character": 9}}}]