fix: binder info range for let rec/where

src/Lean/Elab/LetRec.lean

@@ -59,13 +59,13 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         else
           liftMacroM $ expandMatchAltsIntoMatch decl decl[3]
       pure {
-        ref           := decl,
-        attrs         := attrs,
-        shortDeclName := shortDeclName,
-        declName      := declName,
-        binderIds     := binderIds,
-        type          := type,
-        mvar          := mvar,
+        ref           := declId
+        attrs         := attrs
+        shortDeclName := shortDeclName
+        declName      := declName
+        binderIds     := binderIds
+        type          := type
+        mvar          := mvar
         valStx        := valStx
         : LetRecDeclView }
     else
@@ -120,7 +120,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
   let view ← mkLetRecDeclView stx
   withAuxLocalDecls view.decls fun fvars => do
     for decl in view.decls, fvar in fvars do
-      addTermInfo (isBinder := true) decl.ref[0] fvar
+      addTermInfo (isBinder := true) decl.ref fvar
     let values ← elabLetRecDeclValues view
     let body ← elabTermEnsuringType view.body expectedType?
     registerLetRecsToLift view.decls fvars values

tests/lean/infoTree.lean.expected.out

@@ -390,5 +390,5 @@ infoTree.lean:44:0: error: expected stx
         _uniq.862 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
       _uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
         _uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
-  f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 45⟩
+  f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
   f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩

tests/lean/letrec1.lean.expected.out

@@ -1,4 +1,4 @@
 letrec1.lean:6:0-9:7: error: 'f1.g' has already been declared
 letrec1.lean:18:35-18:36: error: unknown identifier 'g'
-letrec1.lean:27:8-28:9: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously
-letrec1.lean:37:10-37:50: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously
+letrec1.lean:27:8-27:9: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously
+letrec1.lean:37:10-37:11: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously

tests/lean/letrecErrors.lean.expected.out

@@ -1,3 +1,3 @@
-letrecErrors.lean:2:10-2:30: error: 'f1.g' has already been declared
-letrecErrors.lean:11:12-11:32: error: 'f2.h' has already been declared
+letrecErrors.lean:2:10-2:11: error: 'f1.g' has already been declared
+letrecErrors.lean:11:12-11:13: error: 'f2.h' has already been declared
 letrecErrors.lean:18:2-19:5: error: 'f3.h' has already been declared