feat: improve error message "don't know how to synthesize implicit argument"

src/Lean/Elab/Term.lean

@@ -374,14 +374,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := d
   match mvarErrorInfo.kind with
   | MVarErrorKind.implicitArg app => do
     let app ← instantiateMVars app
-    let f    := app.getAppFn
-    let args := app.getAppArgs
-    let msg  := args.foldl (init := "@" ++ MessageData.ofExpr f) fun (msg : MessageData) (arg : Expr) =>
-      if arg.getAppFn.isMVar then
-        msg ++ " " ++ arg.getAppFn
-      else
-        msg ++ " …"
-    let msg : MessageData := m!"don't know how to synthesize implicit argument{indentD msg}"
+    let msg : MessageData := m!"don't know how to synthesize implicit argument{indentExpr app.setAppPPExplicit}"
     let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
     logErrorAt mvarErrorInfo.ref msg
   | MVarErrorKind.hole => do

tests/lean/defaultInstance.lean.expected.out

@@ -1,7 +1,7 @@
 defaultInstance.lean:20:20: error: failed to synthesize instance
   Foo Bool (?m x)
 defaultInstance.lean:20:20: error: don't know how to synthesize implicit argument
-  @f … ?m ?m …
+  @f Bool (?m x) ?m x
 context:
 x : Bool
 ⊢ Type
@@ -9,7 +9,7 @@ defaultInstance.lean:20:17: error: failed to infer definition type
 defaultInstance.lean:22:35: error: failed to create type class instance for 
   Foo Bool (?m x)
 defaultInstance.lean:22:35: error: don't know how to synthesize implicit argument
-  @f … ?m ?m …
+  @f Bool (?m x) (?m x) x
 context:
 x : Bool
 ⊢ Type

tests/lean/evalWithMVar.lean.expected.out

@@ -1,6 +1,6 @@
 Sum.someRight c : Option Nat
 evalWithMVar.lean:13:6: error: don't know how to synthesize implicit argument
-  @Sum.someRight ?m … …
+  @Sum.someRight ?m Nat c
 context:
 ⊢ Type _
 evalWithMVar.lean:13:20: error: don't know how to synthesize implicit argument

tests/lean/holes.lean.expected.out

@@ -11,12 +11,12 @@ x : Nat
 y : Nat := g x + g x
 ⊢ Nat
 holes.lean:10:15: error: don't know how to synthesize implicit argument
-  @g … ?m …
+  @g Nat (?m x) x
 context:
 x : Nat
 ⊢ Type
 holes.lean:10:9: error: don't know how to synthesize implicit argument
-  @g … ?m …
+  @g Nat (?m x) x
 context:
 x : Nat
 ⊢ Type