feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors

src/frontends/lean/elaborator.cpp

@@ -153,6 +153,11 @@ auto elaborator::mk_pp_ctx() -> pp_fn {
     return ::lean::mk_pp_ctx(m_ctx.env(), m_opts, m_ctx.mctx(), m_ctx.lctx());
 }
 
+formatter elaborator::mk_fmt_ctx() {
+    auto pp_fn = mk_pp_ctx();
+    return formatter(m_opts, [=](expr const & e, options const &) { return pp_fn(e); });
+}
+
 format elaborator::pp_indent(pp_fn const & pp_fn, expr const & e) {
     unsigned i = get_pp_indent(m_opts);
     return nest(i, line() + pp_fn(e));
@@ -344,7 +349,7 @@ level elaborator::get_level(expr const & A, expr const & ref) {
     }
 
     auto pp_fn = mk_pp_ctx();
-    throw elaborator_exception(ref, format("type expected at") + pp_indent(pp_fn, A));
+    throw elaborator_exception(ref, pp_type_expected(mk_fmt_ctx(), A, &A_type));
 }
 
 level elaborator::replace_univ_placeholder(level const & l) {
@@ -776,8 +781,7 @@ expr elaborator::ensure_function(expr const & e, expr const & ref) {
     if (auto r = mk_coercion_to_fn(e, e_type, ref)) {
         return *r;
     }
-    auto pp_fn = mk_pp_ctx();
-    throw elaborator_exception(ref, format("function expected at") + pp_indent(pp_fn, e));
+    throw elaborator_exception(ref, pp_function_expected(mk_fmt_ctx(), e, e_type));
 }
 
 expr elaborator::ensure_type(expr const & e, expr const & ref) {
@@ -794,8 +798,7 @@ expr elaborator::ensure_type(expr const & e, expr const & ref) {
         return *r;
     }
 
-    auto pp_fn = mk_pp_ctx();
-    report_or_throw(elaborator_exception(ref, format("type expected at") + pp_indent(pp_fn, e)));
+    report_or_throw(elaborator_exception(ref, pp_type_expected(mk_fmt_ctx(), e, &e_type)));
     // only create the metavar if can actually recover from the error
     return mk_sorry(some_expr(mk_sort(mk_univ_metavar())), ref);
 }

src/frontends/lean/elaborator.h

@@ -105,6 +105,7 @@ private:
 
     typedef std::function<format(expr const &)> pp_fn;
     pp_fn mk_pp_ctx();
+    formatter mk_fmt_ctx();
     format pp_indent(pp_fn const & pp_fn, expr const & e);
     format pp_indent(expr const & e);
     format pp(expr const & e);

src/kernel/error_msgs.cpp

@@ -13,12 +13,27 @@ format pp_indent_expr(formatter const & fmt, expr const & e) {
     return nest(get_pp_indent(fmt.get_options()), compose(line(), fmt(e)));
 }
 
-format pp_type_expected(formatter const & fmt, expr const & e) {
-    return compose(format("type expected at"), pp_indent_expr(fmt, e));
+format pp_type_expected(formatter const & fmt, expr const & e, expr const * e_type) {
+    format f = format("type expected at") + pp_indent_expr(fmt, e);
+    if (e_type) {
+        f += line() + format("term has type") + pp_indent_expr(fmt, *e_type);
+    }
+    return f;
 }
 
-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 & fn) {
+    return format("function expected at") + pp_indent_expr(fmt, fn);
+}
+
+format pp_function_expected(formatter const & fmt, expr const & fn, expr const & fn_type) {
+    return pp_function_expected(fmt, fn) +
+           line() + format("term has type") + pp_indent_expr(fmt, fn_type);
+}
+
+format pp_function_expected(formatter const & fmt, expr const & app, expr const & fn, expr const & fn_type) {
+    return pp_function_expected(fmt, app) +
+            line() + format("term") + pp_indent_expr(fmt, get_app_fn(fn)) +
+            line() + format("has type") + pp_indent_expr(fmt, fn_type);
 }
 
 static list<options> * g_distinguishing_pp_options = nullptr;

src/kernel/error_msgs.h

@@ -9,8 +9,10 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 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_type_expected(formatter const & fmt, expr const & e, expr const * fn_type = nullptr);
+format pp_function_expected(formatter const & fmt, expr const & fn);
+format pp_function_expected(formatter const & fmt, expr const & fn, expr const & fn_type);
+format pp_function_expected(formatter const & fmt, expr const & app, expr const & fn, expr const & fn_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

@@ -50,7 +50,7 @@ expr type_checker::ensure_sort_core(expr e, expr const & s) {
     if (is_sort(new_e)) {
         return new_e;
     } else {
-        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_type_expected(fmt, s); });
+        throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_type_expected(fmt, s, &e); });
     }
 }
 

src/library/type_context.cpp

@@ -1238,9 +1238,7 @@ expr type_context::infer_app(expr const & e) {
             f_type = whnf(instantiate_rev(f_type, i-j, args.data()+j));
             if (!is_pi(f_type)) {
                 throw generic_exception(e, [=](formatter const & fmt) {
-                        return format("infer type failed, function expected at") + pp_indent_expr(fmt, e)
-                            + line() + format("term") + pp_indent_expr(fmt, f)
-                            + line() + format("has type") + pp_indent_expr(fmt, f_type);
+                        return format("infer type failed, ") + pp_function_expected(fmt, e, f, f_type);
                     });
             }
             f_type = binding_body(f_type);

tests/lean/bad_error3.lean.expected.out

@@ -1,11 +1,15 @@
 bad_error3.lean:1:33: error: type expected at
   p 0
+term has type
+  ℕ → Prop
 bad_error3.lean:3:0: error: tactic failed, there are unsolved goals
 state:
 p : ℕ → ℕ → Prop
 ⊢ ⁇
 bad_error3.lean:5:32: error: type expected at
   p 0
+term has type
+  ℕ → Prop
 bad_error3.lean:7:0: error: tactic failed, there are unsolved goals
 state:
 p : ℕ → ℕ → Prop

tests/lean/elab12.lean.expected.out

@@ -1,20 +1,30 @@
 elab12.lean:1:33: error: type expected at
   0
+term has type
+  ℕ
 elab12.lean:1:41: error: function expected at
   rfl
+term has type
+  ?m_2 = ?m_2
 Additional information:
 elab12.lean:1:41: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
   too many arguments
 elab12.lean:2:2: error: function expected at
   H
+term has type
+  ⁇
 λ (a : ℕ), have H : ⁇, from ⁇, ⁇ : ∀ (a : ℕ), a = a
 elab12.lean:4:45: error: function expected at
   rfl
+term has type
+  ?m_2 = ?m_2
 Additional information:
 elab12.lean:4:45: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
   too many arguments
 elab12.lean:5:2: error: function expected at
   H
+term has type
+  a = a
 λ (a : ℕ), have H : a = a, from ⁇, ⁇ : ∀ (a : ℕ), a = a
 elab12.lean:7:47: error: invalid have-expression, expression
   a + 0
@@ -24,8 +34,12 @@ but is expected to have type
   a = a
 elab12.lean:8:2: error: function expected at
   H
+term has type
+  a = a
 λ (a : ℕ), have H : a = a, from ⁇, ⁇ : ∀ (a : ℕ), a = a
 elab12.lean:11:2: error: function expected at
   H
+term has type
+  a = a
 λ (a : ℕ), have H : a = a, from rfl, ⁇ : ∀ (a : ℕ), a = a
 λ (a : ℕ), have H : a = a, from rfl, H : ∀ (a : ℕ), a = a

tests/lean/elab4.lean.expected.out

@@ -7,10 +7,14 @@ failed to synthesize type class instance for
 error for foo.f
 function expected at
   foo.f 0 1
+term has type
+  ?m_1
 
 error for boo.f
 function expected at
   boo.f 0 1 2
+term has type
+  ℕ
 Additional information:
 elab4.lean:13:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
 elab4.lean:15:7: error: ambiguous overload, possible interpretations

tests/lean/elab4b.lean.expected.out

@@ -6,10 +6,14 @@ failed to synthesize type class instance for
 error for foo.f
 function expected at
   f 0 1
+term has type
+  ?m_1
 
 error for boo.f
 function expected at
   f 0 1 2
+term has type
+  ℕ
 Additional information:
 elab4b.lean:9:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
 elab4b.lean:11:7: error: ambiguous overload, possible interpretations

tests/lean/elab_error_recovery.lean.expected.out

@@ -43,4 +43,6 @@ nat.succ (nat.succ (nat.succ (nat.succ ⁇)))
 2
 elab_error_recovery.lean:22:13: error: type expected at
   0
+term has type
+  ℕ
 ∀ (x : ⁇), x = x : Prop

tests/lean/error_pos.lean.expected.out

@@ -1,16 +1,26 @@
 error_pos.lean:1:39: error: type expected at
   B
+term has type
+  A → Type
 error_pos.lean:1:0: warning: declaration '[anonymous]' uses sorry
 error_pos.lean:4:43: error: type expected at
   B
+term has type
+  A → Type
 error_pos.lean:9:40: error: type expected at
   B
+term has type
+  A → Type
 λ (A : Type) (B : A → Type) (b : ⁇), true : Π (A : Type), (A → Type) → ⁇ → Prop
 error_pos.lean:11:36: error: type expected at
   B
+term has type
+  A → Type
 λ (A : Type) (B : A → Type), ⁇ → true : Π (A : Type), (A → Type) → Prop
 error_pos.lean:13:43: error: type expected at
   B
+term has type
+  A → Type
 λ (A : Type) (B : A → Type) (b : ⁇), b : Π (A : Type), (A → Type) → ⁇ → ⁇
 error_pos.lean:15:105: error: invalid let-expression, expression
   a₁

tests/lean/inaccessible.lean.expected.out

@@ -1,14 +1,20 @@
 inaccessible.lean:14:10: error: function expected at
   mk
+term has type
+  ?m_1
 inaccessible.lean:14:4: error: invalid use of inaccessible term, it is not fixed by other arguments
 inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
 inaccessible.lean:17:4: error: invalid use of inaccessible term, it is not fixed by other arguments
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:25:3: error: function expected at
   f
+term has type
+  ?m_1
 inaccessible.lean:25:16: error: ill-formed match/equations expression
 inaccessible.lean:28:3: error: function expected at
   f
+term has type
+  ?m_1
 inaccessible.lean:28:16: error: ill-formed match/equations expression
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments

tests/lean/inaccessible2.lean.expected.out

@@ -6,10 +6,16 @@ inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be
 inaccessible2.lean:11:46: error: invalid expression
 inaccessible2.lean:11:4: error: function expected at
   f
+term has type
+  ?m_1
 inaccessible2.lean:11:11: error: function expected at
   ⁇
+term has type
+  ?m_1
 inaccessible2.lean:11:2: error: function expected at
   inv_3 .?m_1 ⁇
+term has type
+  A
 inaccessible2.lean:11:46: error: ill-formed match/equations expression
 inaccessible2.lean:11:46: error: command expected
 inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible

tests/lean/interactive/correct_snapshot_invalidation.input.expected.out

@@ -1,11 +1,11 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"message":"file invalidated","response":"ok","seq_num":1}
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":2}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo\ntermhas type\n  Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"msgs":[],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"},{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}

tests/lean/local_notation_bug2.lean.expected.out

@@ -1,4 +1,6 @@
 local_notation_bug2.lean:7:9: error: invalid antiquotation, occurs outside of quoted expressions
 local_notation_bug2.lean:7:8: error: function expected at
   5
+term has type
+  ?m_1
 ⁇

tests/lean/string_imp.lean.expected.out

@@ -3,7 +3,11 @@ string_imp.lean:1:4: error: equation compiler failed (use 'set_option trace.eqn_
 string_imp.lean:5:3: error: invalid pattern: variable, constructor or constant tagged as pattern expected
 string_imp.lean:5:3: error: function expected at
   string_imp.mk
+term has type
+  _
 string_imp.lean:4:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 string_imp.lean:8:0: error: unknown identifier 'string_imp.cases_on'
 string_imp.lean:8:0: error: function expected at
   ⁇
+term has type
+  ?m_1

tests/lean/user_command.lean.expected.out

@@ -4,6 +4,8 @@ user_command.lean:14:0: error: unknown identifier 'foo'
 user_command.lean:12:5: error: invalid user-defined command, must return type `lean.parser unit`
 user_command.lean:12:50: error: function expected at
   ()
+term has type
+  unit
 foo
 user_command.lean:23:8: error: command does not accept modifiers
 bar