Improve application type mismatch error messages

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

src/frontends/lean/lean_elaborator.cpp

@@ -331,7 +331,7 @@ class elaborator::imp {
                                 modified = true;
                                 args[i] = mk_app(coercion, args[i]);
                             } else {
-                                throw app_type_mismatch_exception(m_env, ctx, e, i, expected, given);
+                                throw app_type_mismatch_exception(m_env, ctx, e, types.size(), types.data());
                             }
                         }
                     }
@@ -722,17 +722,6 @@ public:
     format pp(formatter & f, options const & o) const {
         format r;
         bool first = true;
-        for (unsigned i = 0; i < m_metavars.size(); i++) {
-            metavar_info const & info = m_metavars[i];
-            expr m = ::lean::mk_metavar(i);
-            if (first) first = false; else r += line();
-            format r_assignment;
-            if (info.m_assignment)
-                r_assignment = f(info.m_assignment, o);
-            else
-                r_assignment = highlight(format("[unassigned]"));
-            r += group(format{f(m,o), space(), g_assignment_fmt, line(), r_assignment});
-        }
         for (auto c : m_constraints) {
             if (first) first = false; else r += line();
             r += group(format{f(c.m_lhs, o), space(), g_unification_fmt, line(), f(c.m_rhs, o)});

src/kernel/kernel_exception.h

@@ -90,22 +90,17 @@ public:
     have type get_expected_type().
 */
 class app_type_mismatch_exception : public type_checker_exception {
-    context  m_context;
-    expr     m_app;
-    unsigned m_arg_pos;
-    expr     m_expected_type;
-    expr     m_given_type;
+    context           m_context;
+    expr              m_app;
+    std::vector<expr> m_arg_types;
 public:
-    app_type_mismatch_exception(environment const & env, context const & ctx, expr const & app, unsigned pos, expr const & expected, expr const & given):
-        type_checker_exception(env), m_context(ctx), m_app(app), m_arg_pos(pos),
-        m_expected_type(expected), m_given_type(given) {}
+    app_type_mismatch_exception(environment const & env, context const & ctx, expr const & app, unsigned num, expr const * arg_types):
+        type_checker_exception(env), m_context(ctx), m_app(app), m_arg_types(arg_types, arg_types+num) {}
     virtual ~app_type_mismatch_exception() {}
     context const & get_context() const { return m_context; }
     expr const & get_application() const { return m_app; }
     virtual expr const & get_main_expr() const { return get_application(); }
-    unsigned get_arg_pos() const { return m_arg_pos; }
-    expr const & get_expected_type() const { return m_expected_type; }
-    expr const & get_given_type() const { return m_given_type; }
+    std::vector<expr> const & get_arg_types() const { return m_arg_types; }
     virtual char const * what() const noexcept { return "application argument type mismatch"; }
 };
 

src/kernel/type_checker.cpp

@@ -40,10 +40,6 @@ class type_checker::imp {
         throw function_expected_exception(m_env, ctx, s);
     }
 
-    expr infer_pi(expr const & e, context const & ctx) {
-        return check_pi(infer_type(e, ctx), e, ctx);
-    }
-
 public:
     imp(environment const & env):
         m_env(env),
@@ -82,15 +78,19 @@ public:
             r = mk_type(ty_level(e) + 1);
             break;
         case expr_kind::App: {
-            expr f_t     = infer_pi(arg(e, 0), ctx);
-            unsigned i   = 1;
             unsigned num = num_args(e);
             lean_assert(num >= 2);
+            buffer<expr> arg_types;
+            for (unsigned i = 0; i < num; i++) {
+                arg_types.push_back(infer_type(arg(e, i), ctx));
+            }
+            expr f_t     = check_pi(arg_types[0], e, ctx);
+            unsigned i   = 1;
             while (true) {
-                expr const & c = arg(e, i);
-                expr c_t       = infer_type(c, ctx);
+                expr const & c   = arg(e, i);
+                expr const & c_t = arg_types[i];
                 if (!m_normalizer.is_convertible(abst_domain(f_t), c_t, ctx))
-                    throw app_type_mismatch_exception(m_env, ctx, e, i, abst_domain(f_t), c_t);
+                    throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
                 else if (closed(c))

src/library/formatter.cpp

@@ -45,15 +45,26 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
     } 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);
-        format given_f = operator()(_ex->get_context(), _ex->get_given_type(), false, opts);
-        format expected_f = operator()(_ex->get_context(), _ex->get_expected_type(), false, opts);
-        unsigned arg_pos = _ex->get_arg_pos();
-        return format({format("type mismatch at application argument"), space(), format(arg_pos), space(), format("of"),
+        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 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));
+        }
+        format arg_type_msg;
+        if (arg_types.size() > 2)
+            arg_type_msg = format("arguments types");
+        else
+            arg_type_msg = format("argument type");
+        return format({format("type mismatch at application"),
                     nest(indent, compose(line(), app_f)),
-                    line(), format("expected type"),
-                    nest(indent, compose(line(), expected_f)),
-                    line(), format("given type"),
-                    nest(indent, compose(line(), given_f))});
+                    line(), format("function type"),
+                    nest(indent, compose(line(), f_type_fmt)),
+                    line(), arg_type_msg,
+                    arg_types_fmt});
     } else if (function_expected_exception const * _ex = dynamic_cast<function_expected_exception const *>(&ex)) {
         unsigned indent = get_pp_indent(opts);
         format expr_f = operator()(_ex->get_context(), _ex->get_expr(), false, opts);

src/tests/frontends/lean/implicit_args.cpp

@@ -40,12 +40,8 @@ static void success(expr const & e, expr const & expected, frontend const & env)
         std::cout << infer_type(elaborate(e, env), env) << "\n";
     } catch (app_type_mismatch_exception & ex) {
         context const & ctx = ex.get_context();
-        std::cout << "Application type mismatch at argument " << ex.get_arg_pos() << "\n"
-                  << "  " << mk_pair(ex.get_application(), ctx) << "\n"
-                  << "expected type\n"
-                  << "  " << mk_pair(ex.get_expected_type(), ctx) << "\n"
-                  << "given type\n"
-                  << "  " << mk_pair(ex.get_given_type(), ctx) << "\n";
+        std::cout << "Application type mismatch at\n"
+                  << "  " << mk_pair(ex.get_application(), ctx) << "\n";
         lean_unreachable();
     }
 }

tests/lean/ex2.lean.expected.out

@@ -7,11 +7,12 @@ Error (line: 8, pos: 0) invalid object declaration, environment already has an o
   Assumed: b
 and a b
   Assumed: A
-Error (line: 12, pos: 11) type mismatch at application argument 2 of
+Error (line: 12, pos: 11) type mismatch at application
     and a A
-expected type
+function type
+    Bool -> Bool -> Bool
+arguments types
     Bool
-given type
     Type
 Variable A : Type
 ⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩

tests/lean/ex3.lean

@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable myeq : Pi (A : Type), A -> A -> Bool
 Show myeq _ true false
 Variable T : Type

tests/lean/ex3.lean.expected.out

@@ -1,18 +1,23 @@
+  Set: pp::colors
   Assumed: myeq
 myeq Bool ⊤ ⊥
   Assumed: T
   Assumed: a
-Error (line: 5, pos: 6) type mismatch at application argument 3 of
+Error (line: 6, pos: 6) type mismatch at application
     myeq Bool ⊤ a
-expected type
+function type
+    Π (A : Type) (_ _ : A), Bool
+arguments types
+    Type
     Bool
-given type
     T
   Assumed: myeq2
   Set: lean::pp::implicit
-Error (line: 9, pos: 15) type mismatch at application argument 3 of
+Error (line: 10, pos: 15) type mismatch at application
     myeq2::explicit Bool ⊤ a
-expected type
+function type
+    Π (A : Type) (a b : A), Bool
+arguments types
+    Type
     Bool
-given type
     T

tests/lean/tst7.lean.expected.out

@@ -4,8 +4,6 @@
 Error (line: 5, pos: 40) application type mismatch during term elaboration at term
     f B a
 Elaborator state
-    ?M0 := [unassigned]
-    ?M1 := [unassigned]
     #0 ≈ lift:0:2 ?M0
   Assumed: myeq
 myeq (Π (A : Type) (a : A), A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)

tests/lean/tst9.lean

@@ -1,3 +1,4 @@
+Set pp::colors false
 Variable f : Pi A : Type, A -> A -> A
 Variable N : Type
 Variable g : N -> N -> Bool

tests/lean/tst9.lean.expected.out

@@ -1,10 +1,12 @@
+  Set: pp::colors
   Assumed: f
   Assumed: N
   Assumed: g
   Assumed: a
-Error (line: 5, pos: 6) type mismatch at application argument 1 of
+Error (line: 6, pos: 6) type mismatch at application
     g ⊤ (f _ a a)
-expected type
-    N
-given type
+function type
+    N → N → Bool
+arguments types
     Bool
+    ?M0