From f97e238b8ee6cd3a6ccbf4f04cd10da98bdce539 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Sep 2016 15:00:45 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): decorate error messages when overloads are used --- src/frontends/lean/elaborator.cpp | 130 ++++++++++++++------- src/frontends/lean/elaborator.h | 8 +- tests/lean/choice_expl.lean.expected.out | 2 + tests/lean/elab11.lean.expected.out | 22 ++++ tests/lean/elab4.lean.expected.out | 6 + tests/lean/elab4b.lean.expected.out | 6 + tests/lean/nary_overload.lean.expected.out | 2 + tests/lean/over_notation.lean.expected.out | 2 + 8 files changed, 131 insertions(+), 47 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index fd96719af1..b1a6a78adb 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1125,7 +1125,7 @@ expr elaborator::visit_overload_candidate(expr const & fn, buffer const & return visit_base_app_core(fn, arg_mask::Default, args, true, expected_type, ref); } -void elaborator::throw_no_overload_applicable(buffer const & fns, buffer const & error_msgs, expr const & ref) { +format elaborator::mk_no_overload_applicable_msg(buffer const & fns, buffer const & error_msgs) { format r("none of the overloads are applicable"); lean_assert(error_msgs.size() == fns.size()); for (unsigned i = 0; i < fns.size(); i++) { @@ -1135,48 +1135,12 @@ void elaborator::throw_no_overload_applicable(buffer const & fns, buffer elaborator::visit_overloaded_app_with_expected(buffer const & fns, buffer const & args, - expr const & expected_type, expr const & ref) { - snapshot S(*this); - buffer> candidates; - // TODO(Leo): use error messages to decorate nested exceptions - buffer error_msgs; - for (expr const & fn : fns) { - try { - // Restore state - S.restore(*this); - bool has_args = !args.empty(); - expr new_fn = visit_function(fn, has_args, ref); - first_pass_info info; - first_pass(new_fn, args, expected_type, ref, info); - candidates.emplace_back(new_fn, snapshot(*this), info); - } catch (elaborator_exception & ex) { - error_msgs.push_back(ex); - } catch (exception & ex) { - error_msgs.push_back(elaborator_exception(ref, format(ex.what()))); - } - } - - if (candidates.empty()) { - S.restore(*this); - return none_expr(); - } - - if (candidates.size() == 1) { - // Restore successful state - auto & c = candidates[0]; - expr fn = std::get<0>(c); - std::get<1>(c).restore(*this); - first_pass_info & info = std::get<2>(c); - return some_expr(second_pass(fn, args, ref, info)); - } - - /* Failed to disambiguate using expected type, switch to basic */ - S.restore(*this); - return none_expr(); +void elaborator::throw_no_overload_applicable(buffer const & fns, buffer const & error_msgs, + expr const & ref) { + throw elaborator_exception(ref, mk_no_overload_applicable_msg(fns, error_msgs)); } expr elaborator::visit_overloaded_app_core(buffer const & fns, buffer const & args, @@ -1243,16 +1207,94 @@ expr elaborator::visit_overloaded_app_core(buffer const & fns, buffer const & fns, buffer const & args, + expr const & expected_type, expr const & ref) { + snapshot S(*this); + buffer> candidates; + buffer error_msgs; + for (expr const & fn : fns) { + try { + // Restore state + S.restore(*this); + bool has_args = !args.empty(); + expr new_fn = visit_function(fn, has_args, ref); + first_pass_info info; + first_pass(new_fn, args, expected_type, ref, info); + candidates.emplace_back(new_fn, snapshot(*this), info); + } catch (elaborator_exception & ex) { + error_msgs.push_back(ex); + } catch (exception & ex) { + error_msgs.push_back(elaborator_exception(ref, format(ex.what()))); + } + } + + if (candidates.empty()) { + try { + /* Failed to disambiguate using expected type, switch to basic */ + S.restore(*this); + return visit_overloaded_app_core(fns, args, some_expr(expected_type), ref); + } catch (elaborator_exception & ex) { + auto pp_fn = mk_pp_ctx(); + format msg = format("switched to basic overload resolution where arguments are elaborated without " + "any information about the expected type, because failed to elaborate all candidates " + "using the expected type"); + msg += pp_indent(pp_fn, expected_type); + msg += line() + format("this can happen because, for example, coercions were not considered in the process"); + msg += line() + mk_no_overload_applicable_msg(fns, error_msgs); + throw nested_elaborator_exception(ref, ex, msg); + } + } + + if (candidates.size() == 1) { + // Restore successful state + auto & c = candidates[0]; + expr fn = std::get<0>(c); + std::get<1>(c).restore(*this); + first_pass_info & info = std::get<2>(c); + try { + return second_pass(fn, args, ref, info); + } catch (elaborator_exception & ex) { + auto pp_fn = mk_pp_ctx(); + format msg = format("overload was disambiguated using expected type"); + msg += line() + pp_overloads(pp_fn, fns); + msg += line() + format("the only applicable one seemed to be: ") + pp(fn); + throw nested_elaborator_exception(ref, ex, msg); + } + } + + try { + /* Failed to disambiguate using expected type, switch to basic */ + S.restore(*this); + return visit_overloaded_app_core(fns, args, some_expr(expected_type), ref); + } catch (elaborator_exception & ex) { + auto pp_fn = mk_pp_ctx(); + format msg = format("switched to basic overload resolution where arguments are elaborated without " + "any information about the expected type because it failed to disambiguate " + "overload using the expected type"); + msg += pp_indent(pp_fn, expected_type); + msg += line() + format("the following overloaded terms were applicable"); + for (auto const & c : candidates) + msg += pp_indent(pp_fn, std::get<0>(c)); + throw nested_elaborator_exception(ref, ex, msg); + } +} + expr elaborator::visit_overloaded_app(buffer const & fns, buffer const & args, optional const & expected_type, expr const & ref) { trace_elab_detail(tout() << "overloaded application at " << pos_string_for(ref); auto pp_fn = mk_pp_ctx(); tout() << pp_overloads(pp_fn, fns) << "\n";); if (expected_type) { - if (auto r = visit_overloaded_app_with_expected(fns, args, *expected_type, ref)) - return *r; + return visit_overloaded_app_with_expected(fns, args, *expected_type, ref); + } else { + try { + return visit_overloaded_app_core(fns, args, expected_type, ref); + } catch (elaborator_exception & ex) { + format msg = format("switched to basic overload resolution where arguments are elaborated without " + "any information about the expected type because expected type was not available"); + throw nested_elaborator_exception(ref, ex, msg); + } } - return visit_overloaded_app_core(fns, args, expected_type, ref); } expr elaborator::visit_no_confusion_app(expr const & fn, buffer const & args, optional const & expected_type, diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 5009406930..10ffdd136c 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -166,7 +166,8 @@ private: bool is_with_expected_candidate(expr const & fn); struct first_pass_info; - void first_pass(expr const & fn, buffer const & args, expr const & expected_type, expr const & ref, first_pass_info & info); + void first_pass(expr const & fn, buffer const & args, expr const & expected_type, expr const & ref, + first_pass_info & info); expr second_pass(expr const & fn, buffer const & args, expr const & ref, first_pass_info & info); expr visit_base_app_simple(expr const & _fn, arg_mask amask, buffer const & args, bool args_already_visited, optional const & expected_type, expr const & ref); @@ -175,13 +176,14 @@ private: expr visit_base_app(expr const & fn, arg_mask amask, buffer const & args, optional const & expected_type, expr const & ref); void validate_overloads(buffer const & fns, expr const & ref); + format mk_no_overload_applicable_msg(buffer const & fns, buffer const & error_msgs); [[ noreturn ]] void throw_no_overload_applicable(buffer const & fns, buffer const & error_msgs, expr const & ref); expr visit_overload_candidate(expr const & fn, buffer const & args, optional const & expected_type, expr const & ref); - optional visit_overloaded_app_with_expected(buffer const & fns, buffer const & args, - expr const & expected_type, expr const & ref); + expr visit_overloaded_app_with_expected(buffer const & fns, buffer const & args, + expr const & expected_type, expr const & ref); expr visit_overloaded_app_core(buffer const & fns, buffer const & args, optional const & expected_type, expr const & ref); expr visit_overloaded_app(buffer const & fns, buffer const & args, diff --git a/tests/lean/choice_expl.lean.expected.out b/tests/lean/choice_expl.lean.expected.out index 44725fa7eb..c13b3c83d7 100644 --- a/tests/lean/choice_expl.lean.expected.out +++ b/tests/lean/choice_expl.lean.expected.out @@ -3,3 +3,5 @@ pr a b : N choice_expl.lean:15:6: error: ambiguous overload, possible interpretations N2.pr a b N1.pr a b +Additional information: +choice_expl.lean:15:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available diff --git a/tests/lean/elab11.lean.expected.out b/tests/lean/elab11.lean.expected.out index 1133b4b260..fe2b5b1713 100644 --- a/tests/lean/elab11.lean.expected.out +++ b/tests/lean/elab11.lean.expected.out @@ -1,6 +1,8 @@ elab11.lean:6:6: error: ambiguous overload, possible interpretations bla.f 1 boo.f 1 +Additional information: +elab11.lean:6:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available bla.f 1 : ℕ boo.f 1 : bool elab11.lean:16:7: error: none of the overloads are applicable @@ -19,3 +21,23 @@ has type bool but is expected to have type string +Additional information: +elab11.lean:16:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type, because failed to elaborate all candidates using the expected type + string +this can happen because, for example, coercions were not considered in the process +none of the overloads are applicable +error for bla.f +type mismatch + f ?m_1 +has type + ℕ +but is expected to have type + string + +error for boo.f +type mismatch + f ?m_1 +has type + bool +but is expected to have type + string diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out index dcda8659f5..dd0b2cfafc 100644 --- a/tests/lean/elab4.lean.expected.out +++ b/tests/lean/elab4.lean.expected.out @@ -11,12 +11,18 @@ function expected at error for boo.f function expected at boo.f 0 1 2 +Additional information: +elab4.lean:13:6: 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:6: error: ambiguous overload, possible interpretations foo.f 0 1 boo.f 0 1 +Additional information: +elab4.lean:15:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available foo.f bool.tt 2 : bool bla.f bool.tt bool.ff bool.tt : bool → bool elab4.lean:21:6: error: ambiguous overload, possible interpretations bla.f bool.tt bool.ff foo.f bool.tt bool.ff +Additional information: +elab4.lean:21:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available foo.f 0 1 : ℕ diff --git a/tests/lean/elab4b.lean.expected.out b/tests/lean/elab4b.lean.expected.out index 4ba2c13f26..185a9d913f 100644 --- a/tests/lean/elab4b.lean.expected.out +++ b/tests/lean/elab4b.lean.expected.out @@ -10,9 +10,15 @@ function expected at error for boo.f function expected at f 0 1 2 +Additional information: +elab4b.lean:9:6: 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:6: error: ambiguous overload, possible interpretations foo.f 0 1 boo.f 0 1 +Additional information: +elab4b.lean:11:6: 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:13:6: error: ambiguous overload, possible interpretations bla.f bool.tt bool.ff foo.f bool.tt bool.ff +Additional information: +elab4b.lean:13:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available diff --git a/tests/lean/nary_overload.lean.expected.out b/tests/lean/nary_overload.lean.expected.out index 818f28afcb..7ba037e3ec 100644 --- a/tests/lean/nary_overload.lean.expected.out +++ b/tests/lean/nary_overload.lean.expected.out @@ -1,6 +1,8 @@ nary_overload.lean:16:6: error: ambiguous overload, possible interpretations [a, b, c] [a, b, c] +Additional information: +nary_overload.lean:16:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available [a, b, c] : vec A [a, b, c] : lst A @vec.cons A a (@vec.cons A b (@vec.cons A c (@vec.nil A))) : vec.{1} A diff --git a/tests/lean/over_notation.lean.expected.out b/tests/lean/over_notation.lean.expected.out index 3a3f749895..ec2750d8e7 100644 --- a/tests/lean/over_notation.lean.expected.out +++ b/tests/lean/over_notation.lean.expected.out @@ -20,5 +20,7 @@ has type bool but is expected to have type nat +Additional information: +over_notation.lean:11:9: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available f 1 (f 2 (f 3 0)) : nat g "a" (g "b" (g "c" "")) : string