chore(kernel/error_msgs): show inferred type when function expected

src/frontends/lean/elaborator.cpp

@@ -505,7 +505,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
                 coes  = get_coercions_to_fun(env(), f_type);
             }
             if (is_nil(coes)) {
-                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
+                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f, f_type); });
             } else if (is_nil(tail(coes))) {
                 expr old_f = f;
                 f = mk_coercion_app(head(coes), f);
@@ -514,9 +514,9 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
                 save_coercion_info(old_f, f);
                 lean_assert(is_pi(f_type));
             } else {
-                old_local_context ctx      = m_context;
-                justification j        = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) {
-                        return pp_function_expected(fmt, substitution(subst).instantiate(f));
+                old_local_context ctx = m_context;
+                justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) {
+                        return pp_function_expected(fmt, substitution(subst).instantiate(f), substitution(subst).instantiate(f_type));
                     });
                 auto choice_fn = [=](expr const & meta, expr const &, substitution const &) {
                     flet<old_local_context> save1(m_context,      ctx);

src/kernel/default_converter.cpp

@@ -340,7 +340,7 @@ bool default_converter::try_eta_expansion_core(expr const & t, expr const & s, c
         } else if (auto m = m_tc->is_stuck(s_type)) {
             expr r              = mk_pi_for(*m);
             justification j     = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
-                    return pp_function_expected(fmt, substitution(subst).instantiate(s));
+                    return pp_function_expected(fmt, substitution(subst).instantiate(s), substitution(subst).instantiate(s_type));
                 });
             aux_cs += mk_eq_cnstr(s_type, r, j);
             s_type  = r;

src/kernel/error_msgs.cpp

@@ -17,8 +17,12 @@ format pp_type_expected(formatter const & fmt, expr const & e) {
     return compose(format("type expected at"), pp_indent_expr(fmt, e));
 }
 
-format pp_function_expected(formatter const & fmt, expr const & e) {
-    return compose(format("function expected at"), pp_indent_expr(fmt, e));
+format pp_function_expected(formatter const & fmt, expr const & e, expr const & e_type) {
+    format r;
+    r = compose(format("function expected at"), pp_indent_expr(fmt, e));
+    r += line();
+    r += compose(format("which has type"), pp_indent_expr(fmt, e_type));
+    return r;
 }
 
 MK_THREAD_LOCAL_GET_DEF(list<options>, get_distinguishing_pp_options)

src/kernel/error_msgs.h

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 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_function_expected(formatter const & fmt, expr const & e, expr const & e_type);
 format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & fn_type, expr const & arg, expr const & given_type, bool as_error);
 format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type, bool as_error);
 format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type);

src/kernel/type_checker.cpp

@@ -126,11 +126,11 @@ pair<expr, constraint_seq> type_checker::ensure_pi_core(expr e, expr const & s)
     } else if (auto m = is_stuck(ecs.first)) {
         expr r             = mk_pi_for(*m);
         justification j    = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) {
-                return pp_function_expected(fmt, substitution(subst).instantiate(s));
+                return pp_function_expected(fmt, substitution(subst).instantiate(s), substitution(subst).instantiate(ecs.first));
             });
         return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second);
     } else {
-        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_function_expected(fmt, s); });
+        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_function_expected(fmt, s, ecs.first); });
     }
 }
 

tests/lean/function_expected.lean

@@ -0,0 +1,20 @@
+import data.sigma
+open function
+
+namespace Lob
+
+inductive TypeExpr : Type₁ :=
+| Arrow : TypeExpr → TypeExpr → TypeExpr
+| QuotedTermExpr : TypeExpr → TypeExpr
+
+open TypeExpr
+
+inductive TermExpr : TypeExpr → Type :=
+| Lob : ∀ { LT : TypeExpr }, TermExpr (Arrow (QuotedTermExpr LT) LT) → TermExpr LT
+
+open TermExpr
+
+definition denoteTermExpr : Π {typeExpr : TypeExpr}, TermExpr typeExpr → Type₁
+| _ (@Lob typeExpr1 termExpr1) := (denoteTermExpr termExpr1) (Lob termExpr1)
+
+end Lob

tests/lean/function_expected.lean.expected.out

@@ -0,0 +1,4 @@
+function_expected.lean:18:35: error: function expected at
+  denoteTermExpr termExpr1
+which has type
+  Type₁