From d8620ef4c90afb6bc44a404b0467ff25535d9b4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Jun 2015 19:44:00 -0700 Subject: [PATCH] fix(kernel,library,frontends/lean): improve error messages see #669 --- src/frontends/lean/calc_proof_elaborator.cpp | 2 +- src/frontends/lean/elaborator.cpp | 18 +++++----- src/kernel/default_converter.cpp | 2 +- src/kernel/error_msgs.cpp | 37 +++++++++++++++----- src/kernel/error_msgs.h | 4 +-- src/kernel/justification.cpp | 20 +++++------ src/kernel/justification.h | 8 ++--- src/kernel/type_checker.cpp | 22 ++++++------ src/library/kernel_bindings.cpp | 4 +-- src/library/unifier.cpp | 12 +++---- src/library/util.cpp | 4 +-- tests/lean/669.lean.expected.out | 6 ++-- tests/lean/error_pos_bug.lean.expected.out | 6 ++-- tests/lean/mismatch.lean | 3 ++ tests/lean/mismatch.lean.expected.out | 8 +++++ 15 files changed, 92 insertions(+), 64 deletions(-) create mode 100644 tests/lean/mismatch.lean create mode 100644 tests/lean/mismatch.lean.expected.out diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index c50a969dc..413019000 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -61,7 +61,7 @@ static optional> mk_op(environment const & env, local_context & return optional>(); r = mk_app(r, explicit_arg); expr type = tc->infer(explicit_arg, cs); - justification j = mk_app_justification(r, explicit_arg, binding_domain(op_type), type); + justification j = mk_app_justification(r, op_type, explicit_arg, type); if (!tc->is_def_eq(binding_domain(op_type), type, j, cs)) return optional>(); op_type = instantiate(binding_body(op_type), explicit_arg); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 5b948ab5c..7c82bb271 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -318,7 +318,7 @@ expr elaborator::visit_choice(expr const & e, optional const & t, constrai name_generator && /* ngen */) { return choose(std::make_shared(*this, ctx, full_ctx, meta, type, e)); }; - auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) { + auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main, bool) { format r = pp_previous_error_header(fmt, pos_prov, some_expr(e), is_main); r += format("none of the overloads is applicable:"); for (unsigned i = 0; i < get_num_choices(e); i++) { @@ -449,7 +449,7 @@ pair elaborator::ensure_fun(expr f, constraint_seq & cs) { } else { local_context ctx = m_context; local_context full_ctx = m_full_context; - justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(f)); }); auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator &&) { @@ -667,7 +667,7 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { expr a = visit_expecting_type_of(app_arg(e), d_type, a_cs); expr a_type = infer_type(a, a_cs); expr r = mk_app(f, a, e.get_tag()); - justification j = mk_app_justification(r, a, d_type, a_type); + justification j = mk_app_justification(r, f_type, a, a_type); auto new_a_cs = ensure_has_type(a, a_type, d_type, j); expr new_a = new_a_cs.first; cs += f_cs + new_a_cs.second + a_cs; @@ -1175,7 +1175,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { new_cs.linearize(tmp_cs); for (constraint const & c : tmp_cs) { justification j = c.get_justification(); - auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main) { + auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main, bool) { if (!is_main) return format(); format r = j.pp(fmt, pp, s); @@ -1230,12 +1230,12 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) { expr lhs_type = infer_type(new_lhs, cs); expr rhs_type = infer_type(new_rhs, cs); - justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst, bool as_error) { substitution s(subst); name n = local_pp_name(lhs_fn); if (is_match_binder_name(n)) n = "match"; - return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type)); + return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type), as_error); }); pair new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j); new_rhs = new_rhs_cs.first; @@ -1379,7 +1379,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) { } S_mk = mk_app(S_mk, v, result_tag); expr v_type = infer_type(v, cs); - justification j = mk_app_justification(S_mk, v, d_type, v_type); + justification j = mk_app_justification(S_mk, S_mk_type, v, v_type); auto new_v_cs = ensure_has_type(v, v_type, d_type, j); expr new_v = new_v_cs.first; cs += new_v_cs.second; @@ -2062,9 +2062,9 @@ std::tuple elaborator::operator()(expr const & t, constraint_seq v_cs; expr r_v = visit(v, v_cs); expr r_v_type = infer_type(r_v, v_cs); - justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst, bool as_error) { substitution s(subst); - return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type)); + return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type), as_error); }); pair r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j); r_v = r_v_cs.first; diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 9859ef649..8bb6ea06d 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -336,7 +336,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)) { name_generator ngen = m_tc->mk_ngen(); expr r = mk_pi_for(ngen, *m); - justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(s)); }); aux_cs += mk_eq_cnstr(s_type, r, j); diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index a50ce3a93..8804c4afd 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -63,30 +63,51 @@ std::tuple 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 & arg, expr const & expected_type, expr const & given_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) { + formatter fmt(_fmt); format r; format expected_fmt, given_fmt; + lean_assert(is_pi(fn_type)); + if (!is_explicit(binding_info(fn_type))) { + // For implicit arguments to be shown if argument is implicit + options opts = fmt.get_options(); + // TODO(Leo): this is hackish, the option is defined in the folder library + opts = opts.update_if_undef(name{"pp", "implicit"}, true); + fmt = fmt.update_options(opts); + } + expr expected_type = binding_domain(fn_type); std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); - r += format("type mismatch at application"); + if (as_error) + r += format("type mismatch at application"); + else + r += format("application type constraint"); r += pp_indent_expr(fmt, app); r += compose(line(), format("term")); r += pp_indent_expr(fmt, arg); r += compose(line(), format("has type")); r += given_fmt; - r += compose(line(), format("but is expected to have type")); - r += expected_fmt; + if (as_error) { + r += compose(line(), format("but is expected to have type")); + r += expected_fmt; + } return r; } -format pp_def_type_mismatch(formatter const & fmt, name const & n, 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, bool as_error) { format expected_fmt, given_fmt; std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); - format r("type mismatch at definition '"); + format r; + if (as_error) + r += format("type mismatch at definition '"); + else + r += format("definition type constraint '"); r += format(n); r += format("', has type"); r += given_fmt; - r += compose(line(), format("but is expected to have type")); - r += expected_fmt; + if (as_error) { + r += compose(line(), format("but is expected to have type")); + r += expected_fmt; + } return r; } diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index 676608f06..0175ca493 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -11,8 +11,8 @@ 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 & 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_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); /** \brief Set a list extra configuration options that are used to try to distinguish error such as given/expected type mismatch diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 8546d9396..a91d952ee 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -293,7 +293,7 @@ public: }; format justification::pp_core(formatter const & fmt, pos_info_provider const * p, substitution const & s, - justification_set & set, bool is_main) const { + justification_set & set, bool is_main, bool as_error) const { if (set.contains(*this)) return format(); set.insert(*this); @@ -302,25 +302,25 @@ format justification::pp_core(formatter const & fmt, pos_info_provider const * p return format(); switch (it->m_kind) { case justification_kind::Asserted: - return to_asserted(it)->m_fn(fmt, p, s, is_main); + return to_asserted(it)->m_fn(fmt, p, s, is_main, as_error); case justification_kind::Wrapper: - return to_wrapper(it)->m_fn(fmt, p, s, is_main); + return to_wrapper(it)->m_fn(fmt, p, s, is_main, as_error); case justification_kind::Assumption: if (is_main) return format(format("Assumption "), format(to_assumption(it)->m_idx)); else return format(); case justification_kind::Composite: { - format r1 = to_composite(it)->m_child[0].pp_core(fmt, p, s, set, is_main); - format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false); + format r1 = to_composite(it)->m_child[0].pp_core(fmt, p, s, set, is_main, as_error); + format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false, as_error); return r1 + r2; }} lean_unreachable(); } -format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const { +format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s, bool as_error) const { justification_set set; - return pp_core(fmt, p, s, set, true); + return pp_core(fmt, p, s, set, true, as_error); } justification mk_wrapper(justification const & j, optional const & s, pp_jst_fn const & fn) { @@ -346,18 +346,18 @@ justification mk_justification(optional const & s, pp_jst_fn const & fn) { return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s)); } justification mk_justification(optional const & s, pp_jst_sfn const & fn) { - return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst, bool is_main) { + return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst, bool is_main, bool as_error) { // Remark: we are not using to_pos(s, p) anymore because we don't try to display complicated error messages anymore. // return compose(to_pos(s, p), fn(fmt, subst)); if (is_main) - return fn(fmt, subst); + return fn(fmt, subst, as_error); else return format(); }); } justification mk_justification(char const * msg, optional const & s) { std::string _msg(msg); - return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &, bool is_main) { + return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &, bool is_main, bool) { if (is_main) return format(_msg); else diff --git a/src/kernel/justification.h b/src/kernel/justification.h index b8cccbb35..07662d4b9 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -23,7 +23,7 @@ struct justification_cell; The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions to justification objects. */ -typedef std::function pp_jst_fn; +typedef std::function pp_jst_fn; class justification_set; @@ -43,7 +43,7 @@ class justification { justification_cell * m_ptr; justification(justification_cell * ptr); format pp_core(formatter const & fmt, pos_info_provider const * p, substitution const & s, - justification_set & visited, bool is_main) const; + justification_set & visited, bool is_main, bool as_error) const; public: justification(); justification(justification const & s); @@ -66,7 +66,7 @@ public: \brief Convert this justification into a format object. This method is usually used to report "error" messages to users. */ - format pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const; + format pp(formatter const & fmt, pos_info_provider const * p, substitution const & s, bool as_error = true) const; /** \brief Return an expression associated with the justification object. */ @@ -85,7 +85,7 @@ public: /** \brief Simpler version of pp_jst_fn */ -typedef std::function pp_jst_sfn; +typedef std::function pp_jst_sfn; /** \brief Return a format object containing position information for the given expression (if available) */ format to_pos(optional const & e, pos_info_provider const * p); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 6482515b1..af916a8ff 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -106,7 +106,7 @@ pair type_checker::ensure_sort_core(expr e, expr const & s } else if (is_meta(ecs.first)) { expr r = mk_sort(mk_meta_univ(m_gen.next())); justification j = mk_justification(s, - [=](formatter const & fmt, substitution const & subst) { + [=](formatter const & fmt, substitution const & subst, bool) { return pp_type_expected(fmt, substitution(subst).instantiate(s)); }); return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second); @@ -124,7 +124,7 @@ pair type_checker::ensure_pi_core(expr e, expr const & s) return ecs; } else if (auto m = is_stuck(ecs.first)) { expr r = mk_pi_for(m_gen, *m); - justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst, bool) { return pp_function_expected(fmt, substitution(subst).instantiate(s)); }); return to_ecs(r, mk_eq_cnstr(ecs.first, r, j), ecs.second); @@ -136,7 +136,7 @@ pair type_checker::ensure_pi_core(expr e, expr const & s) static constexpr char const * g_macro_error_msg = "failed to type check macro expansion"; justification type_checker::mk_macro_jst(expr const & e) { - return mk_justification(e, [=](formatter const &, substitution const &) { + return mk_justification(e, [=](formatter const &, substitution const &, bool) { return format(g_macro_error_msg); }); } @@ -155,10 +155,10 @@ app_delayed_justification::app_delayed_justification(expr const & e, expr const 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 & arg, expr const & d_type, expr const & a_type) { - auto pp_fn = [=](formatter const & fmt, substitution const & subst) { +justification mk_app_justification(expr const & e, expr const & fn_type, expr const & arg, expr const & a_type) { + auto pp_fn = [=](formatter const & fmt, substitution const & subst, bool as_error) { substitution s(subst); - return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(arg), s.instantiate(d_type), s.instantiate(a_type)); + return pp_app_type_mismatch(fmt, s.instantiate(e), s.instantiate(fn_type), s.instantiate(arg), s.instantiate(a_type), as_error); }; return mk_justification(e, pp_fn); } @@ -167,7 +167,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, m_arg, binding_domain(m_fn_type), m_arg_type); + m_jst = mk_app_justification(m_e, m_fn_type, m_arg, m_arg_type); } return *m_jst; } @@ -264,15 +264,15 @@ pair type_checker::infer_app(expr const & e, bool infer_on pair acs = infer_type_core(app_arg(e), infer_only); expr a_type = acs.first; app_delayed_justification jst(e, app_arg(e), f_type, a_type); - expr d_type = binding_domain(pics.first); + expr d_type = binding_domain(f_type); pair dcs = is_def_eq(a_type, d_type, jst); if (!dcs.first) { throw_kernel_exception(m_env, e, [=](formatter const & fmt) { - return pp_app_type_mismatch(fmt, e, app_arg(e), d_type, a_type); + return pp_app_type_mismatch(fmt, e, f_type, app_arg(e), a_type, true); }); } - return mk_pair(instantiate(binding_body(pics.first), app_arg(e)), + return mk_pair(instantiate(binding_body(f_type), app_arg(e)), pics.second + ftcs.second + dcs.second + acs.second); } else { buffer args; @@ -491,7 +491,7 @@ certified_declaration check(environment const & env, declaration const & d, name expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first; if (!checker2.is_def_eq(val_type, d.get_type()).first) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) { - return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type); + return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true); }); } } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 952befd89..e1180b872 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1402,14 +1402,14 @@ static int mk_justification(lua_State * L) { return push_justification(L, justification()); } else if (nargs == 1) { std::string s = lua_tostring(L, 1); - return push_justification(L, mk_justification(none_expr(), [=](formatter const &, substitution const &) { + return push_justification(L, mk_justification(none_expr(), [=](formatter const &, substitution const &, bool) { return format(s.c_str()); })); } else { std::string s = lua_tostring(L, 1); environment env = to_environment(L, 2); expr e = to_expr(L, 3); - justification j = mk_justification(some_expr(e), [=](formatter const & fmt, substitution const & subst) { + justification j = mk_justification(some_expr(e), [=](formatter const & fmt, substitution const & subst, bool) { expr new_e = substitution(subst).instantiate(e); format r; r += format(s.c_str()); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index d6c8340ea..5e860d32d 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -641,7 +641,7 @@ struct unifier_fn { justification mk_assign_justification(expr const & m, expr const & m_type, expr const & v_type, justification const & j) { auto r = j.get_main_expr(); if (!r) r = m; - justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst) { + justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst, bool) { substitution s(subst); format r; expr _m = s.instantiate(m); @@ -657,8 +657,8 @@ struct unifier_fn { r += given_fmt; r += compose(line(), format("but is expected to have type")); r += expected_fmt; - r += compose(line(), format("the assignment was attempted when trying to solve")); - r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst))); + r += compose(line(), format("the assignment was attempted when processing")); + r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false))); return r; }); return mk_composite1(new_j, j); @@ -712,7 +712,7 @@ struct unifier_fn { justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j, expr const & bad_local) { - justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst) { + justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst, bool) { format r = format("invalid local context when tried to assign"); r += pp_indent_expr(fmt, rhs); buffer locals; @@ -730,8 +730,8 @@ struct unifier_fn { } r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux)); } - r += compose(line(), format("the assignment was attempted when trying to solve")); - r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst))); + r += compose(line(), format("the assignment was attempted when processing")); + r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false))); return r; }); return mk_composite1(new_j, j); diff --git a/src/library/util.cpp b/src/library/util.cpp index 801553700..5507320ba 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -792,7 +792,7 @@ format pp_type_mismatch(formatter const & fmt, expr const & v, expr const & v_ty } justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) { - return mk_justification(src, [=](formatter const & fmt, substitution const & subst) { + return mk_justification(src, [=](formatter const & fmt, substitution const & subst, bool) { substitution s(subst); return pp_type_mismatch(fmt, s.instantiate(v), s.instantiate(v_type), s.instantiate(t)); }); @@ -870,7 +870,7 @@ expr instantiate_meta(expr const & meta, substitution & subst) { } justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) { - return mk_justification(m, [=](formatter const & fmt, substitution const & subst) { + return mk_justification(m, [=](formatter const & fmt, substitution const & subst, bool) { substitution tmp(subst); expr new_m = instantiate_meta(m, tmp); expr new_type = type_checker(env).infer(new_m).first; diff --git a/tests/lean/669.lean.expected.out b/tests/lean/669.lean.expected.out index fdc9a651e..b1811a778 100644 --- a/tests/lean/669.lean.expected.out +++ b/tests/lean/669.lean.expected.out @@ -4,12 +4,10 @@ placeholder has type Type₁ but is expected to have type Prop -the assignment was attempted when trying to solve - type mismatch at application +the assignment was attempted when processing + application type constraint (λ {T : Prop} (t : T), t) bool.tt term bool.tt has type bool - but is expected to have type - bool diff --git a/tests/lean/error_pos_bug.lean.expected.out b/tests/lean/error_pos_bug.lean.expected.out index d925b7884..3f7535ea7 100644 --- a/tests/lean/error_pos_bug.lean.expected.out +++ b/tests/lean/error_pos_bug.lean.expected.out @@ -5,12 +5,10 @@ placeholder has type Category but is expected to have type Type -the assignment was attempted when trying to solve - type mismatch at application +the assignment was attempted when processing + application type constraint Category.mk a (category.mk b c) term category.mk b c has type category a - but is expected to have type - category a diff --git a/tests/lean/mismatch.lean b/tests/lean/mismatch.lean new file mode 100644 index 000000000..eaa1bfd94 --- /dev/null +++ b/tests/lean/mismatch.lean @@ -0,0 +1,3 @@ +definition id {A : Type} {a : A} := a + +check @id nat 1 diff --git a/tests/lean/mismatch.lean.expected.out b/tests/lean/mismatch.lean.expected.out new file mode 100644 index 000000000..c26c9c85c --- /dev/null +++ b/tests/lean/mismatch.lean.expected.out @@ -0,0 +1,8 @@ +mismatch.lean:3:7: error: type mismatch at application + @id nat 1 +term + 1 +has type + num +but is expected to have type + nat