From f8cfc4ea1b784272b69e9b4c7bd31e4bdfd34416 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 17 Jul 2017 18:00:01 +0200 Subject: [PATCH] feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors --- src/frontends/lean/elaborator.cpp | 13 +++++++---- src/frontends/lean/elaborator.h | 1 + src/kernel/error_msgs.cpp | 23 +++++++++++++++---- src/kernel/error_msgs.h | 6 +++-- src/kernel/type_checker.cpp | 2 +- src/library/type_context.cpp | 4 +--- tests/lean/bad_error3.lean.expected.out | 4 ++++ tests/lean/elab12.lean.expected.out | 14 +++++++++++ tests/lean/elab4.lean.expected.out | 4 ++++ tests/lean/elab4b.lean.expected.out | 4 ++++ .../elab_error_recovery.lean.expected.out | 2 ++ tests/lean/error_pos.lean.expected.out | 10 ++++++++ tests/lean/inaccessible.lean.expected.out | 6 +++++ tests/lean/inaccessible2.lean.expected.out | 6 +++++ ...t_snapshot_invalidation.input.expected.out | 8 +++---- .../local_notation_bug2.lean.expected.out | 2 ++ tests/lean/string_imp.lean.expected.out | 4 ++++ tests/lean/user_command.lean.expected.out | 2 ++ 18 files changed, 96 insertions(+), 19 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7543234196..cd2ee04ecd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 8f341b7f4f..24a80fbace 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -105,6 +105,7 @@ private: typedef std::function 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); diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index dd863cc3b3..644d3d0a18 100644 --- a/src/kernel/error_msgs.cpp +++ b/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 * g_distinguishing_pp_options = nullptr; diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index 4cfc13699d..210221416e 100644 --- a/src/kernel/error_msgs.h +++ b/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); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index c3192d7d94..2deba12a2b 100644 --- a/src/kernel/type_checker.cpp +++ b/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); }); } } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 185bdda976..7abe6d3e00 100644 --- a/src/library/type_context.cpp +++ b/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); diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out index ae6fa92935..a8fb7ade66 100644 --- a/tests/lean/bad_error3.lean.expected.out +++ b/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 diff --git a/tests/lean/elab12.lean.expected.out b/tests/lean/elab12.lean.expected.out index 9a96c06ddb..f9c3b4a5f1 100644 --- a/tests/lean/elab12.lean.expected.out +++ b/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 diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out index 799236aa58..0543484cd8 100644 --- a/tests/lean/elab4.lean.expected.out +++ b/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 diff --git a/tests/lean/elab4b.lean.expected.out b/tests/lean/elab4b.lean.expected.out index db239203d8..aab1247a6e 100644 --- a/tests/lean/elab4b.lean.expected.out +++ b/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 diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out index b9f8043761..a57d8110a7 100644 --- a/tests/lean/elab_error_recovery.lean.expected.out +++ b/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 diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out index 60f74b46fa..8e5db04b28 100644 --- a/tests/lean/error_pos.lean.expected.out +++ b/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₁ diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out index 5185a7a4ee..9094778491 100644 --- a/tests/lean/inaccessible.lean.expected.out +++ b/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 diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out index 1f462a9938..55fdc63d71 100644 --- a/tests/lean/inaccessible2.lean.expected.out +++ b/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 diff --git a/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out b/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out index 748dd51c35..4a93be4e8b 100644 --- a/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out +++ b/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"} diff --git a/tests/lean/local_notation_bug2.lean.expected.out b/tests/lean/local_notation_bug2.lean.expected.out index 6ad90a0567..c655074d23 100644 --- a/tests/lean/local_notation_bug2.lean.expected.out +++ b/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 ⁇ diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out index 1dc84065e2..2664cc40b7 100644 --- a/tests/lean/string_imp.lean.expected.out +++ b/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 diff --git a/tests/lean/user_command.lean.expected.out b/tests/lean/user_command.lean.expected.out index b3ea31f733..485c1aa81f 100644 --- a/tests/lean/user_command.lean.expected.out +++ b/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