Improve application type mismatch errors. We also show the implicit arguments (not just their types)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/formatter.cpp

@@ -44,15 +44,18 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
                 format(_ex->get_name()), format("'")};
     } else if (app_type_mismatch_exception const * _ex = dynamic_cast<app_type_mismatch_exception const *>(&ex)) {
         unsigned indent = get_pp_indent(opts);
-        format app_f = operator()(_ex->get_context(), _ex->get_application(), false, opts);
+        context const & ctx = _ex->get_context();
+        expr const & app    = _ex->get_application();
+        format app_fmt      = operator()(ctx, app, false, opts);
         std::vector<expr> const & arg_types = _ex->get_arg_types();
         auto it = arg_types.begin();
-        format f_type_fmt = operator()(_ex->get_context(), *it, false, opts);
+        format f_type_fmt   = operator()(ctx, *it, false, opts);
         format arg_types_fmt;
         ++it;
-        for (; it != arg_types.end(); ++it) {
-            format arg_type_fmt = operator()(_ex->get_context(), *it, false, opts);
-            arg_types_fmt += nest(indent, compose(line(), arg_type_fmt));
+        for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
+            format arg_fmt      = operator()(ctx, arg(app, i), false, opts);
+            format arg_type_fmt = operator()(ctx, *it, false, opts);
+            arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
         }
         format arg_type_msg;
         if (arg_types.size() > 2)
@@ -60,7 +63,7 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
         else
             arg_type_msg = format("Argument type:");
         return format({format("type mismatch at application"),
-                    nest(indent, compose(line(), app_f)),
+                    nest(indent, compose(line(), app_fmt)),
                     line(), format("Function type:"),
                     nest(indent, compose(line(), f_type_fmt)),
                     line(), arg_type_msg,

tests/lean/ex2.lean.expected.out

@@ -15,8 +15,8 @@ Error (line: 13, pos: 11) type mismatch at application
 Function type:
     Bool -> Bool -> Bool
 Arguments types:
-    Bool
-    Type
+    a : Bool
+    A : Type
 Variable A : Type
 (lean::pp::notation := false, pp::unicode := false, pp::colors := false)
 Error (line: 16, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options

tests/lean/ex3.lean.expected.out

@@ -9,9 +9,9 @@ Error (line: 5, pos: 6) type mismatch at application
 Function type:
     Π (A : Type) (_ _ : A), Bool
 Arguments types:
-    Type
-    Bool
-    T
+    Bool : Type
+    ⊤ : Bool
+    a : T
   Assumed: myeq2
   Set: lean::pp::implicit
 Error (line: 9, pos: 15) type mismatch at application
@@ -19,6 +19,6 @@ Error (line: 9, pos: 15) type mismatch at application
 Function type:
     Π (A : Type) (a b : A), Bool
 Arguments types:
-    Type
-    Bool
-    T
+    Bool : Type
+    ⊤ : Bool
+    a : T

tests/lean/tst9.lean.expected.out

@@ -9,5 +9,5 @@ Error (line: 5, pos: 6) type mismatch at application
 Function type:
     N → N → Bool
 Arguments types:
-    Bool
-    ?M0
+    ⊤ : Bool
+    f _ a a : ?M0