feat: improve application type mismatch error message

src/Init/Lean/Elab/Term.lean

@@ -749,19 +749,32 @@ synthesizeSyntheticMVarsAux mayPostpone ()
 
 /--
   If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
-  If they are not, then try coercions. -/
-def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM Expr :=
+  If they are not, then try coercions.
+  Return `some e'` if successful, where `e'` may be different from `e` if coercions have been applied,
+  and `none` otherwise
+ -/
+def tryEnsureHasType? (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) :=
 match expectedType? with
-| none              => pure e
+| none              => pure (some e)
 | some expectedType =>
   condM (isDefEq ref eType expectedType)
-    (pure e)
+    (pure (some e))
     -- TODO try `HasCoe`
-    (let msg : MessageData :=
-       "type mismatch" ++ indentExpr e
-       ++ Format.line ++ "has type" ++ indentExpr eType
-       ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
-     throwError ref msg)
+    (pure none)
+
+/--
+  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
+  If they are not, then try coercions. -/
+def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (eType : Expr) (e : Expr) : TermElabM Expr := do
+e? ← tryEnsureHasType? ref expectedType? eType e;
+match e? with
+| some e => pure e
+| none   =>
+  let msg : MessageData :=
+    "type mismatch" ++ indentExpr e
+    ++ Format.line ++ "has type" ++ indentExpr eType
+    ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType?.get!;
+  throwError ref msg
 
 def mkInstMVar (ref : Syntax) (type : Expr) : TermElabM Expr := do
 mvar ← mkFreshExprMVar ref type MetavarKind.synthetic;

src/Init/Lean/Elab/TermApp.lean

@@ -45,15 +45,21 @@ instMVars.forM $ fun mvarId =>
   unlessM (synthesizeInstMVarCore ref mvarId) $
     registerSyntheticMVar ref mvarId SyntheticMVarKind.typeClass
 
-private def elabArg (ref : Syntax) (arg : Arg) (expectedType : Expr) : TermElabM Expr :=
+private def ensureArgType (ref : Syntax) (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
+argType ← inferType ref arg;
+arg? ← tryEnsureHasType? ref expectedType argType arg;
+match arg? with
+| some arg => pure arg
+| none     => do
+  env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
+  throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f arg { env := env, mctx := mctx, lctx := lctx, opts := opts }
+
+private def elabArg (ref : Syntax) (f : Expr) (arg : Arg) (expectedType : Expr) : TermElabM Expr :=
 match arg with
-| Arg.expr val => do
-  valType ← inferType ref val;
-  ensureHasType ref expectedType valType val
+| Arg.expr val => ensureArgType ref f val expectedType
 | Arg.stx val  => do
   val ← elabTerm val expectedType;
-  valType ← inferType ref val;
-  ensureHasType ref expectedType valType val
+  ensureArgType ref f val expectedType
 
 private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool)
     : Nat → Array NamedArg → Array MVarId → Expr → Expr → TermElabM Expr
@@ -71,12 +77,12 @@ private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedTy
     | some idx => do
       let arg := namedArgs.get! idx;
       let namedArgs := namedArgs.eraseIdx idx;
-      argElab ← elabArg ref arg.val d;
+      argElab ← elabArg ref e arg.val d;
       elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 argElab) (mkApp e argElab)
     | none =>
       let processExplictArg : Unit → TermElabM Expr := fun _ => do {
         if h : argIdx < args.size then do
-          argElab ← elabArg ref (args.get ⟨argIdx, h⟩) d;
+          argElab ← elabArg ref e (args.get ⟨argIdx, h⟩) d;
           elabAppArgsAux (argIdx + 1) namedArgs instMVars (b.instantiate1 argElab) (mkApp e argElab)
         else match d.getOptParamDefault? with
           | some defVal => elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 defVal) (mkApp e defVal)

tests/lean/run/frontend1.lean

@@ -222,3 +222,5 @@ def three := 3
 
 #eval run "#check (fun stx => if True then let e := stx; HasPure.pure e else HasPure.pure stx : Nat → Id Nat)"
 #eval run "constant n : Nat #check n"
+
+#eval fail "#check Nat.succ 'a'"