feat: jump to definition for match pattern variables

src/Lean/Elab/Match.lean

@@ -605,16 +605,30 @@ where
 /--
   Save pattern information in the info tree, and remove `patternWithRef?` annotations.
 -/
-def savePatternInfo (p : Expr) : TermElabM Expr :=
-  withReader (fun ctx => { ctx with inPattern := false }) do
-    let post (e : Expr) : TermElabM TransformStep := do
-      if let some (stx, e) := patternWithRef? e then
-        -- TODO: track whether we are inside of an inaccessible, and set `isBinder`
-        addTermInfo' stx e
-        return .done e
+partial def savePatternInfo (p : Expr) : TermElabM Expr :=
+  go p |>.run false
+where
+  /- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/
+  go (p : Expr) : ReaderT Bool TermElabM Expr := do
+    match p with
+    | .forallE n d b bi => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
+    | .lam n d b bi     => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
+    | .letE n t v b ..  => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
+    | .app f a _        => return mkApp (← go f) (← go a)
+    | .proj _ _ b _     => return p.updateProj! (← go b)
+    | .mdata k b _      =>
+      if inaccessible? p |>.isSome then
+        return mkMData k (← withReader (fun _ => false) (go b))
+      else if let some (stx, p) := patternWithRef? p then
+        let p ← go p
+        if p.isFVar && !(← read) then
+          /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
+          addTermInfo stx p (isBinder := true)
+        else
+          addTermInfo stx p
       else
-        return .done e
-    transform p (post := post)
+        return mkMData k (← go b)
+    | _ => return p
 
 /--
   Main method for `withDepElimPatterns`.

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

@@ -46,11 +46,11 @@ a : α
     @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
     a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
     [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.652]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.653]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-    α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+    α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
     Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-    a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+    a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
     ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
     [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
     Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -59,9 +59,9 @@ a : α
     [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.684]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.685]]]) @ ⟨10, 4⟩-⟨10, 12⟩
     Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+    n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
     Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-    a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+    a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
     n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
       n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
   @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩

tests/lean/infoTree.lean.expected.out

@@ -216,8 +216,9 @@
                 [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
                 [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
                 Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
-                z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
-                w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
+                Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
+                z (isBinder := true) : Nat @ ⟨23, 9⟩-⟨23, 10⟩
+                w (isBinder := true) : Nat @ ⟨23, 12⟩-⟨23, 13⟩
                 (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
                 let z1 := z + w;
                 z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl

tests/lean/interactive/discrsIssue.lean.expected.out

@@ -2,5 +2,4 @@
  "position": {"line": 32, "character": 18}}
 {"range":
  {"start": {"line": 32, "character": 18}, "end": {"line": 32, "character": 20}},
- "goal":
- "e a b : Expr\nh₁ : HasType a Ty.nat\nh₂ : HasType b Ty.nat\n⊢ HasType a Ty.nat"}
+ "goal": "e a b : Expr\nh₁ : HasType a Ty.nat\n⊢ HasType a Ty.nat"}