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

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

src/frontends/lean/elaborator.cpp

@@ -743,7 +743,7 @@ public:
     expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) {
         expr a = app_arg(e);
         expr m = mk_meta(some_expr(d_type), a.get_tag());
-        justification j = mk_app_justification(e, d_type, a_type);
+        justification j = mk_app_justification(e, a, d_type, a_type);
         add_cnstr(mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic)));
         return update_app(e, app_fn(e), m);
     }
@@ -803,7 +803,7 @@ public:
         } else if (is_meta(a_type) && has_coercions_to(d_type)) {
             return mk_delayed_coercion(r, d_type, a_type);
         } else {
-            app_delayed_justification j(r, f_type, a_type);
+            app_delayed_justification j(r, a, f_type, a_type);
             if (!m_tc[m_relax_main_opaque]->is_def_eq(a_type, d_type, j)) {
                 expr new_a = apply_coercion(a, a_type, d_type);
                 bool coercion_worked = false;
@@ -818,7 +818,7 @@ public:
                         // rely on unification hints to solve this constraint
                         add_cnstr(mk_eq_cnstr(a_type, d_type, j.get(), m_relax_main_opaque));
                     } else {
-                        throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
+                        throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, a, d_type, a_type); });
                     }
                 }
             }

src/kernel/error_msgs.cpp

@@ -47,15 +47,17 @@ std::tuple<format, format> pp_until_different(formatter const & fmt, expr const
     return pp_until_different(fmt, e1, e2, get_distinguishing_pp_options());
 }
 
-format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type) {
+format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & arg, expr const & expected_type, expr const & given_type) {
     format r;
     format expected_fmt, given_fmt;
     std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type);
     r += format("type mismatch at application");
     r += pp_indent_expr(fmt, app);
-    r += compose(line(), format("expected type:"));
+    r += compose(line(), format("term"));
+    r += pp_indent_expr(fmt, arg);
+    r += compose(line(), format("is expected of type"));
     r += expected_fmt;
-    r += compose(line(), format("given type:"));
+    r += compose(line(), format("but is given type"));
     r += given_fmt;
     return r;
 }
@@ -65,9 +67,9 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const &
     std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type);
     format r("type mismatch at definition '");
     r += format(n);
-    r += format("', expected type");
+    r += format("', it is expected of type");
     r += expected_fmt;
-    r += compose(line(), format("given type:"));
+    r += compose(line(), format("but is given type"));
     r += given_fmt;
     return r;
 }

src/kernel/error_msgs.h

@@ -11,7 +11,7 @@ namespace lean {
 format pp_indent_expr(formatter const & fmt, expr const & e);
 format pp_type_expected(formatter const & fmt, expr const & e);
 format pp_function_expected(formatter const & fmt, expr const & e);
-format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type);
+format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & arg, expr const & expected_type, expr const & given_type);
 format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type);
 format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type);
 

src/kernel/type_checker.cpp

@@ -181,13 +181,13 @@ void type_checker::check_level(level const & l, expr const & s) {
         throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
 }
 
-app_delayed_justification::app_delayed_justification(expr const & e, expr const & f_type, expr const & a_type):
-    m_e(e), m_fn_type(f_type), m_arg_type(a_type) {}
+app_delayed_justification::app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type):
+    m_e(e), m_arg(arg), m_fn_type(f_type), m_arg_type(a_type) {}
 
-justification mk_app_justification(expr const & e, expr const & d_type, expr const & a_type) {
+justification mk_app_justification(expr const & e, expr const & arg, expr const & d_type, expr const & a_type) {
     auto pp_fn = [=](formatter const & fmt, substitution const & subst) {
         substitution s(subst);
-        return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(d_type), s.instantiate(a_type));
+        return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(arg), s.instantiate(d_type), s.instantiate(a_type));
     };
     return mk_justification(e, pp_fn);
 }
@@ -196,7 +196,7 @@ justification app_delayed_justification::get() {
     if (!m_jst) {
         // We should not have a reference to this object inside the closure.
         // So, we create the following locals that will be captured by the closure instead of 'this'.
-        m_jst = mk_app_justification(m_e, binding_domain(m_fn_type), m_arg_type);
+        m_jst = mk_app_justification(m_e, m_arg, binding_domain(m_fn_type), m_arg_type);
     }
     return *m_jst;
 }
@@ -283,11 +283,11 @@ expr type_checker::infer_app(expr const & e, bool infer_only) {
     if (!infer_only) {
         expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), e);
         expr a_type = infer_type_core(app_arg(e), infer_only);
-        app_delayed_justification jst(e, f_type, a_type);
+        app_delayed_justification jst(e, app_arg(e), f_type, a_type);
         if (!is_def_eq(a_type, binding_domain(f_type), jst)) {
             throw_kernel_exception(m_env, e,
                                    [=](formatter const & fmt) {
-                                       return pp_app_type_mismatch(fmt, e, binding_domain(f_type), a_type);
+                                       return pp_app_type_mismatch(fmt, e, app_arg(e), binding_domain(f_type), a_type);
                                    });
         }
         return instantiate(binding_body(f_type), app_arg(e));

src/kernel/type_checker.h

@@ -208,7 +208,7 @@ certified_declaration check(environment const & env, declaration const & d, name
     \brief Create a justification for an application \c e where the expected type must be \c d_type and
     the argument type is \c a_type.
 */
-justification mk_app_justification(expr const & e, expr const & d_type, expr const & a_type);
+justification mk_app_justification(expr const & e, expr const & arg, expr const & d_type, expr const & a_type);
 
 /**
    \brief Create a justification for a application type mismatch,
@@ -216,11 +216,12 @@ justification mk_app_justification(expr const & e, expr const & d_type, expr con
 */
 class app_delayed_justification : public delayed_justification {
     expr const & m_e;
+    expr const & m_arg;
     expr const & m_fn_type;
     expr const & m_arg_type;
     optional<justification> m_jst;
 public:
-    app_delayed_justification(expr const & e, expr const & f_type, expr const & a_type);
+    app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type);
     virtual justification get();
 };
 }

tests/lean/bug1.lean.expected.out

@@ -1,19 +1,19 @@
-bug1.lean:9:7: error: type mismatch at definition 'and_intro', expected type
+bug1.lean:9:7: error: type mismatch at definition 'and_intro', it is expected of type
   ∀ (p q : bool),
     p → q → a
-given type:
+but is given type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
-bug1.lean:13:7: error: type mismatch at definition 'and_intro', expected type
+bug1.lean:13:7: error: type mismatch at definition 'and_intro', it is expected of type
   ∀ (p q : bool),
     p → q → and p p
-given type:
+but is given type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
-bug1.lean:17:7: error: type mismatch at definition 'and_intro', expected type
+bug1.lean:17:7: error: type mismatch at definition 'and_intro', it is expected of type
   ∀ (p q : bool),
     p → q → and q p
-given type:
+but is given type
   ∀ (p q : bool),
     p → q → (∀ (c : bool), (p → q → c) → c)
 and_intro : ∀ (p q : bool), p → q → and p q

tests/lean/crash.lean.expected.out

@@ -1,7 +1,9 @@
 crash.lean:8:12: error: type mismatch at application
   have H' : not P, from H,
   _
-expected type:
+term
+  H
+is expected of type
   not P
-given type:
+but is given type
   P

tests/lean/let1.lean.expected.out

@@ -27,9 +27,12 @@ let1.lean:16:10: error: type mismatch at application
         λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
           H q (λ (H1 : p) (H2 : q), H2)
   in and_intro
-expected type:
+term
+  λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+    H H1 H2
+is expected of type
   ∀ (p q : Prop),
     p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
-given type:
+but is given type
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)

tests/lean/t10.lean.expected.out

@@ -1,9 +1,11 @@
 ite (and p q) (f x) y : N
 t10.lean:14:6: error: type mismatch at application
   ite (and p q) q
-expected type:
+term
+  q
+is expected of type
   N
-given type:
+but is given type
   B
 cons x (cons y (cons z (cons x (cons y (cons y nil))))) : list
 cons x nil : list