feat: improve auto implicit binder names in definitions/theorems

src/Lean/Elab/MutualDef.lean

@@ -122,7 +122,7 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
           Term.synthesizeSyntheticMVarsNoPostponing
           let (binderIds, xs) := xs.unzip
           let xs ← addAutoBoundImplicits xs
-          let type ← mkForallFVars xs type
+          let type ← mkForallFVars' xs type
           let type ← instantiateMVars type
           let levelNames ← getLevelNames
           if view.type?.isSome then

src/Lean/Meta/ForEachExpr.lean

@@ -60,4 +60,46 @@ def forEachExpr (e : Expr) (f : Expr → MetaM Unit) : MetaM Unit :=
     f e
     pure true
 
+/--
+  Similar to `mkForallFVars`, but tries to infer better binder names when `xs` contains metavariables.
+  Let `?m` be a metavariable in `xs` s.t. `?m` does not have a user facing name.
+  Then, we try to find an application `f ... ?m` in the other binder typer and `type`, and
+  (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for `?m`.
+  The "renaming" is temporary.
+-/
+def mkForallFVars' (xs : Array Expr) (type : Expr) : MetaM Expr := do
+  if (← xs.anyM shouldInferBinderName) then
+    let toReset ← IO.mkRef #[]
+    try
+      for x in xs do
+        visit (← inferType x) toReset
+      visit type toReset
+      mkForallFVars xs type
+    finally
+      for mvarId in (← toReset.get) do
+        modifyMCtx fun mctx => mctx.setMVarUserNameTemporarily mvarId Name.anonymous
+  else
+    mkForallFVars xs type
+where
+  shouldInferBinderName (x : Expr) : MetaM Bool := do
+    match x with
+    | .mvar mvarId _ => return (← Meta.getMVarDecl mvarId).userName.isAnonymous
+    | _ => return false
+
+  visit (e : Expr) (toReset : IO.Ref (Array MVarId)) : MetaM Unit := do
+    forEachExpr (← instantiateMVars e) fun e => do
+      if e.isApp then
+        let args := e.getAppArgs
+        for i in [:args.size] do
+          let arg := args[i]
+          if arg.isMVar && xs.contains arg then
+            let mvarId := arg.mvarId!
+            if (← Meta.getMVarDecl mvarId).userName.isAnonymous then
+              forallBoundedTelescope (← inferType e.getAppFn) (some (i+1)) fun xs _ => do
+                if i < xs.size then
+                  let mvarId := arg.mvarId!
+                  let userName ← mkFreshUserName (← getFVarLocalDecl xs[i]).userName
+                  toReset.modify (·.push mvarId)
+                  modifyMCtx fun mctx => mctx.setMVarUserNameTemporarily mvarId userName
+
 end Lean.Meta

src/Lean/MetavarContext.lean

@@ -349,6 +349,9 @@ def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) :
   let decl := mctx.getDecl mvarId
   { mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } }
 
+/--
+  Set the metavariable user facing name.
+-/
 def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext :=
   let decl := mctx.getDecl mvarId
   { mctx with
@@ -357,6 +360,16 @@ def setMVarUserName (mctx : MetavarContext) (mvarId : MVarId) (userName : Name)
       let userNames := mctx.userNames.erase decl.userName
       if userName.isAnonymous then userNames else userNames.insert userName mvarId }
 
+/--
+  Low-level version of `setMVarUserName`.
+  It does not update the table `userNames`. Thus, `findUserName?` cannot see the modification.
+  It is meant for `mkForallFVars'` where we temporarily set the user facing name of metavariables to get more
+  meaningful binder names.
+-/
+def setMVarUserNameTemporarily (mctx : MetavarContext) (mvarId : MVarId) (userName : Name) : MetavarContext :=
+  let decl := mctx.getDecl mvarId
+  { mctx with decls := mctx.decls.insert mvarId { decl with userName := userName } }
+
 /- Update the type of the given metavariable. This function assumes the new type is
    definitionally equal to the current one -/
 def setMVarType (mctx : MetavarContext) (mvarId : MVarId) (type : Expr) : MetavarContext :=

tests/lean/autoBoundErrorMsg.lean.expected.out

@@ -1,7 +1,7 @@
 autoBoundErrorMsg.lean:1:43-1:44: error: don't know how to synthesize placeholder
 context:
 α : Sort u_1
-x✝ : Sort u_2
-a b : x✝
+α✝ : Sort u_2
+a b : α✝
 h : ∀ {a b : α}, a = b
 ⊢ a = b

tests/lean/autoImplicitChain.lean.expected.out

@@ -1,2 +1,2 @@
-def f : {x : A} → {x_1 : B x} → {c : @C x x_1} → @D x x_1 c → Bool :=
-fun {x} {x_1} {c} d => true
+def f : {a : A} → {a_1 : B a} → {c : @C a a_1} → @D a a_1 c → Bool :=
+fun {a} {a_1} {c} d => true

tests/lean/autoImplicitChainNameIssue.lean

@@ -0,0 +1,12 @@
+inductive Palindrome : List α → Prop where
+  | nil      : Palindrome []
+  | single   : (a : α) → Palindrome [a]
+  | sandwish : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
+
+theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
+  induction h with
+  | nil => done
+  | single a => exact Palindrome.single a
+  | sandwish a h ih => simp; exact Palindrome.sandwish _ ih
+
+#check @palindrome_reverse

tests/lean/autoImplicitChainNameIssue.lean.expected.out

@@ -0,0 +1,6 @@
+autoImplicitChainNameIssue.lean:8:11-8:15: error: unsolved goals
+case nil
+α✝ : Type u_1
+as : List α✝
+⊢ Palindrome (List.reverse [])
+@palindrome_reverse : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)