feat: clean up binder annotations inside of let rec definitions

src/Lean/Elab/LetRec.lean

@@ -95,7 +95,7 @@ private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : A
 
 private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
   view.decls.mapM fun view => do
-    forallBoundedTelescope view.type view.binderIds.size fun xs type => do
+    forallBoundedTelescope view.type view.binderIds.size (cleanupAnnotations := true) fun xs type => do
       -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
       for h : i in *...view.binderIds.size do
         addLocalVarInfo view.binderIds[i] xs[i]!

src/Lean/Elab/MutualDef.lean

@@ -965,30 +965,18 @@ structure LetRecClosure where
 private def mkLetRecClosureFor (toLift : LetRecToLift) (freeVars : Array FVarId) : TermElabM LetRecClosure := do
   let lctx := toLift.lctx
   withLCtx lctx toLift.localInstances do
-  lambdaTelescope toLift.val fun xs val => do
-    /-
-      Recall that `toLift.type` and `toLift.value` may have different binder annotations.
-      See issue #1377 for an example.
-    -/
-    let userNameAndBinderInfos ← forallBoundedTelescope toLift.type xs.size fun xs _ =>
-      xs.mapM fun x => do
-        let localDecl ← x.fvarId!.getDecl
-        return (localDecl.userName, localDecl.binderInfo)
-    /- Auxiliary map for preserving binder user-facing names and `BinderInfo` for types. -/
-    let mut userNameBinderInfoMap : FVarIdMap (Name × BinderInfo) := {}
-    for x in xs, (userName, bi) in userNameAndBinderInfos do
-      userNameBinderInfoMap := userNameBinderInfoMap.insert x.fvarId! (userName, bi)
-    let type ← instantiateForall toLift.type xs
+  /-
+    Recall that `toLift.type` and `toLift.value` may have different binder annotations.
+    See issue #1377 for an example.
+  -/
+  let lambdaArity := toLift.val.getNumHeadLambdas
+  forallBoundedTelescope toLift.type lambdaArity fun xs type => do
+    let val := toLift.val.beta xs
     let lctx ← getLCtx
     let s ← mkClosureFor freeVars <| xs.map fun x => lctx.get! x.fvarId!
-    /- Apply original type binder info and user-facing names to local declarations. -/
-    let typeLocalDecls := s.localDecls.map fun localDecl =>
-      if let some (userName, bi) := userNameBinderInfoMap.get? localDecl.fvarId then
-        localDecl.setBinderInfo bi |>.setUserName userName
-      else
-        localDecl
-    let type := Closure.mkForall typeLocalDecls <| Closure.mkForall s.newLetDecls type
-    let val  := Closure.mkLambda s.localDecls <| Closure.mkLambda s.newLetDecls val
+    let cleanLocalDecls := s.localDecls.map fun decl => decl.setType <| decl.type.cleanupAnnotations
+    let type := Closure.mkForall s.localDecls <| Closure.mkForall s.newLetDecls type
+    let val  := Closure.mkLambda cleanLocalDecls <| Closure.mkLambda s.newLetDecls val
     let c    := mkAppN (Lean.mkConst toLift.declName) s.exprArgs
     toLift.mvarId.assign c
     return {

tests/lean/run/cleanupTypeAnnotations.lean

@@ -9,7 +9,7 @@ set_option pp.mvars false
 Test definitions, theorems, and instances. (MutualDef elaborator)
 Both scope variables and header variables are handled.
 -/
-
+section
 variable (a := true)
 
 /--
@@ -115,3 +115,37 @@ f : optParam Nat 0 → Nat := fun x => x
 example : True :=
   let f (x : Nat := 0) := by trace_state; exact x
   by trace_state; trivial
+
+end
+
+/-!
+Let rec, both as `where` and as real `let rec`.
+-/
+/--
+trace: n✝ : Nat
+x : Bool
+n : Nat
+⊢ Nat
+-/
+#guard_msgs in
+def bar := go 1000
+where
+  go (n : Nat) (x := true) := match n with
+    | 0 => 0
+    | n+1 => by trace_state; exact go n + 1
+/--
+trace: n✝ : Nat
+x : Bool
+n : Nat
+⊢ Nat
+-/
+#guard_msgs in
+def bar' :=
+  let rec go (n : Nat) (x := true) := match n with
+    | 0 => 0
+    | n+1 => by trace_state; exact go n + 1
+  go 1000
+/-- info: bar.go (n : Nat) (x : Bool := true) : Nat -/
+#guard_msgs in #check bar.go
+/-- info: bar'.go (n : Nat) (x : Bool := true) : Nat -/
+#guard_msgs in #check bar'.go