feat(kernel/type_checker): improve application type mismatch error messages

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

src/kernel/kernel_exception.cpp

@@ -43,7 +43,7 @@ format app_type_mismatch_exception::pp(formatter const & fmt, options const & op
         arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
     }
     format r;
-    r += format("type mismatch at application");
+    r += format{format("type mismatch in argument #"), format(m_arg_pos),  format(" at application")};
     r += nest(indent, compose(line(), app_fmt));
     r += compose(line(), format("Function type:"));
     r += nest(indent, compose(line(), f_type_fmt));

src/kernel/kernel_exception.h

@@ -127,18 +127,21 @@ public:
 class app_type_mismatch_exception : public type_checker_exception {
     context           m_context;
     expr              m_app;
+    unsigned          m_arg_pos;
     std::vector<expr> m_arg_types;
 public:
-    app_type_mismatch_exception(ro_environment const & env, context const & ctx, expr const & app, unsigned num, expr const * arg_types):
+    app_type_mismatch_exception(ro_environment const & env, context const & ctx, expr const & app, unsigned arg_pos,
-        type_checker_exception(env), m_context(ctx), m_app(app), m_arg_types(arg_types, arg_types+num) {}
+                                unsigned num, expr const * arg_types):
+        type_checker_exception(env), m_context(ctx), m_app(app), m_arg_pos(arg_pos), 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 optional<expr> get_main_expr() const { return some_expr(get_application()); }
+    unsigned get_arg_pos() const { return m_arg_pos; }
     std::vector<expr> const & get_arg_types() const { return m_arg_types; }
     virtual char const * what() const noexcept { return "application argument type mismatch"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual exception * clone() const { return new app_type_mismatch_exception(m_env, m_context, m_app, m_arg_types.size(), m_arg_types.data()); }
+    virtual exception * clone() const { return new app_type_mismatch_exception(m_env, m_context, m_app, m_arg_pos, m_arg_types.size(), m_arg_types.data()); }
     virtual void rethrow() const { throw *this; }
 };
 

src/kernel/type_checker.cpp

@@ -234,7 +234,7 @@ class type_checker::imp {
                     // thunk for creating justification object if needed
                     auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); };
                     if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification))
-                        throw app_type_mismatch_exception(env(), ctx, e, arg_types.size(), arg_types.data());
+                        throw app_type_mismatch_exception(env(), ctx, e, i, arg_types.size(), arg_types.data());
                     f_t = pi_body_at(f_t, c);
                     i++;
                     if (i == num)

tests/lean/ex2.lean.expected.out

@@ -10,7 +10,7 @@ ex2.lean:8:0: error: invalid object declaration, environment already has an obje
   Assumed: b
 and a b
   Assumed: A
-ex2.lean:12:8: error: type mismatch at application
+ex2.lean:12:8: error: type mismatch in argument #2 at application
     and a A
 Function type:
     Bool -> Bool -> Bool

tests/lean/kernel_ex1.lean.expected.out

@@ -7,7 +7,7 @@ kernel_ex1.lean:3:14: error: type expected, got
 kernel_ex1.lean:4:6: error: function expected at
     a a
   Assumed: f
-kernel_ex1.lean:6:6: error: type mismatch at application
+kernel_ex1.lean:6:6: error: type mismatch in argument #1 at application
     f (λ x : N, x)
 Function type:
     N → N

tests/lean/tst9.lean.expected.out

@@ -4,7 +4,7 @@
   Assumed: N
   Assumed: g
   Assumed: a
-tst9.lean:5:6: error: type mismatch at application
+tst9.lean:5:6: error: type mismatch in argument #1 at application
     g ⊤ (f ?M::0 a a)
 Function type:
     N → N → Bool