From 5568085ab9b22709659eb7ed791f6c0b7513cdc6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Aug 2015 20:31:43 +0100 Subject: [PATCH] fix(frontends/lean/elaborator): closes #771 Produce nicer error message when type/goal is a metavariable and universe metavariables have already been instantiated with universe parameters. --- src/frontends/lean/elaborator.cpp | 42 ++++++++++++++-------- src/frontends/lean/elaborator.h | 10 +++--- tests/lean/626a.lean.expected.out | 24 ++----------- tests/lean/626c.lean.expected.out | 60 +++---------------------------- tests/lean/771.lean | 12 +++++++ tests/lean/771.lean.expected.out | 1 + 6 files changed, 52 insertions(+), 97 deletions(-) create mode 100644 tests/lean/771.lean create mode 100644 tests/lean/771.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 42009c99a..5c1574792 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1148,7 +1148,8 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) { name_generator && ngen) { substitution new_s = s; expr new_eqns = new_s.instantiate_all(eqns); - new_eqns = solve_unassigned_mvars(new_s, new_eqns); + bool reject_type_is_meta = false; + new_eqns = solve_unassigned_mvars(new_s, new_eqns, reject_type_is_meta); if (display_unassigned_mvars(new_eqns, new_s)) return lazy_list(); type_checker_ptr tc = mk_type_checker(_env, std::move(ngen)); @@ -1930,7 +1931,9 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr } } -void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited) { +// The parameters univs_fixed is true if the elaborator has instantiated the universe metavariables with universe parameters. +// See issue #771 +void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta) { if (visited.contains(mlocal_name(mvar))) return; visited.insert(mlocal_name(mvar)); @@ -1941,7 +1944,11 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set // TODO(Leo): we are discarding constraints here expr type = m_tc->infer(*meta).first; // first solve unassigned metavariables in type - type = solve_unassigned_mvars(subst, type, visited); + type = solve_unassigned_mvars(subst, type, visited, reject_type_is_meta); + if (reject_type_is_meta && is_meta(type)) { + throw_elaborator_exception("failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) " + "(solution: provide type explicitly)", mvar); + } proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child()); if (auto pre_tac = get_pre_tactic_for(mvar)) { if (is_begin_end_annotation(*pre_tac)) { @@ -2027,17 +2034,17 @@ static void visit_unassigned_mvars(expr const & e, std::function & new_params) { +expr elaborator::apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params, bool is_def_value) { expr r = s.instantiate(e); if (has_univ_metavar(r)) r = univ_metavars_to_params(env(), lls(), s, univ_params, new_params, r); - r = solve_unassigned_mvars(s, r); + bool reject_type_is_meta = is_def_value; + r = solve_unassigned_mvars(s, r, reject_type_is_meta); display_unassigned_mvars(r, s); return r; } -std::tuple elaborator::apply(substitution & s, expr const & e) { +std::tuple elaborator::apply(substitution & s, expr const & e, bool is_def_value) { auto ps = collect_univ_params(e); buffer new_ps; - expr r = apply(s, e, ps, new_ps); + expr r = apply(s, e, ps, new_ps, is_def_value); return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); } @@ -2153,7 +2161,8 @@ auto elaborator::operator()(list const & ctx, expr const & e, bool _ensure auto p = solve(cs).pull(); lean_assert(p); substitution s = p->first.first; - auto result = apply(s, r); + bool is_value = false; + auto result = apply(s, r, is_value); check_sort_assignments(s); instantiate_info(s); check_used_local_tactic_hints(); @@ -2179,8 +2188,10 @@ std::tuple elaborator::operator()(expr const & t, substitution s = p->first.first; name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t)); buffer new_params; - expr new_r_t = apply(s, r_t, univ_params, new_params); - expr new_r_v = apply(s, r_v, univ_params, new_params); + bool is_value = false; + expr new_r_t = apply(s, r_t, univ_params, new_params, is_value); + is_value = true; + expr new_r_v = apply(s, r_v, univ_params, new_params, is_value); check_sort_assignments(s); instantiate_info(s); check_used_local_tactic_hints(); @@ -2255,7 +2266,8 @@ elaborate_result elaborator::elaborate_nested(list const & ctx, optionalfirst.first; constraints rcs = p->first.second; r = new_subst.instantiate_all(r); - r = solve_unassigned_mvars(new_subst, r); + bool reject_type_is_meta = false; + r = solve_unassigned_mvars(new_subst, r, reject_type_is_meta); rcs = map(rcs, [&](constraint const & c) { return instantiate_metavars(c, new_subst); }); instantiate_info(new_subst); if (report_unassigned) diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 3059c5850..e16aa86c2 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -164,13 +164,13 @@ class elaborator : public coercion_info_manager { bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, expr const & pre_tac, tactic const & tac, bool show_failure); bool try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac); - void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited); - expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited); - expr solve_unassigned_mvars(substitution & subst, expr const & e); + void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited, bool reject_type_is_meta); + expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited, bool reject_type_is_meta); + expr solve_unassigned_mvars(substitution & subst, expr const & e, bool reject_type_is_meta); bool display_unassigned_mvars(expr const & e, substitution const & s); void check_sort_assignments(substitution const & s); - expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params); - std::tuple apply(substitution & s, expr const & e); + expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params, bool is_def_value); + std::tuple apply(substitution & s, expr const & e, bool is_def_value); elaborate_result elaborate_nested(list const & ctx, optional const & expected_type, expr const & e, bool use_tactic_hints, substitution const &, bool report_unassigned); diff --git a/tests/lean/626a.lean.expected.out b/tests/lean/626a.lean.expected.out index fc63afb35..dff37a317 100644 --- a/tests/lean/626a.lean.expected.out +++ b/tests/lean/626a.lean.expected.out @@ -1,22 +1,2 @@ -626a.lean:3:42: error: don't know how to synthesize placeholder -c : C¹ -⊢ ?M_1 -626a.lean:3:44: error: don't know how to synthesize placeholder -c : C¹ -⊢ Π (a : nat), - ?M_1 → ?M_1 -626a.lean:3:29: error: failed to add declaration 'foo.foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : C¹), - nat.rec_on c ?M_2 ?M_3 -626a.lean:8:42: error: don't know how to synthesize placeholder -c : C¹ -⊢ ?M_1 -626a.lean:8:44: error: don't know how to synthesize placeholder -c : C¹ -⊢ Π (a : C¹), - ?M_1 → ?M_1 -626a.lean:8:29: error: failed to add declaration 'boo.foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : C¹), - nat.rec_on c ?M_2 ?M_3 +626a.lean:3:42: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) +626a.lean:8:42: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) diff --git a/tests/lean/626c.lean.expected.out b/tests/lean/626c.lean.expected.out index ce5c3cfa7..0e51411bf 100644 --- a/tests/lean/626c.lean.expected.out +++ b/tests/lean/626c.lean.expected.out @@ -1,55 +1,5 @@ -626c.lean:2:40: error: don't know how to synthesize placeholder -c : C⁽ -⊢ ?M_1 -626c.lean:2:42: error: don't know how to synthesize placeholder -c : C⁽ -⊢ Π (a : C⁽), - ?M_1 → ?M_1 -626c.lean:2:27: error: failed to add declaration 'foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : C⁽), - nat.rec_on c ?M_2 ?M_3 -626c.lean:5:40: error: don't know how to synthesize placeholder -c : α⁽ -⊢ ?M_1 -626c.lean:5:42: error: don't know how to synthesize placeholder -c : α⁽ -⊢ Π (a : α⁽), - ?M_1 → ?M_1 -626c.lean:5:27: error: failed to add declaration 'foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : α⁽), - nat.rec_on c ?M_2 ?M_3 -626c.lean:8:40: error: don't know how to synthesize placeholder -c : _⁽ -⊢ ?M_1 -626c.lean:8:42: error: don't know how to synthesize placeholder -c : _⁽ -⊢ Π (a : _⁽), - ?M_1 → ?M_1 -626c.lean:8:27: error: failed to add declaration 'foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : _⁽), - nat.rec_on c ?M_2 ?M_3 -626c.lean:11:41: error: don't know how to synthesize placeholder -c : C.⁽ -⊢ ?M_1 -626c.lean:11:43: error: don't know how to synthesize placeholder -c : C.⁽ -⊢ Π (a : C.⁽), - ?M_1 → ?M_1 -626c.lean:11:28: error: failed to add declaration 'foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : C.⁽), - nat.rec_on c ?M_2 ?M_3 -626c.lean:14:42: error: don't know how to synthesize placeholder -c : C⁽C⁽ -⊢ ?M_1 -626c.lean:14:44: error: don't know how to synthesize placeholder -c : C⁽C⁽ -⊢ Π (a : C⁽C⁽), - ?M_1 → ?M_1 -626c.lean:14:29: error: failed to add declaration 'foo' to environment, value has metavariables -remark: set 'formatter.hide_full_terms' to false to see the complete term - λ (c : C⁽C⁽), - nat.rec_on c ?M_2 ?M_3 +626c.lean:2:40: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) +626c.lean:5:40: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) +626c.lean:8:40: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) +626c.lean:11:41: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) +626c.lean:14:42: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly) diff --git a/tests/lean/771.lean b/tests/lean/771.lean new file mode 100644 index 000000000..1bd2cdad1 --- /dev/null +++ b/tests/lean/771.lean @@ -0,0 +1,12 @@ +set_option pp.all true +definition id_1 (n : nat) := + by exact n + +definition id_2 (n : nat) := + (by exact n : nat) + +definition id_3 (n : nat) : nat := +by exact n + +definition id_4 (n : nat) := +show nat, by exact n diff --git a/tests/lean/771.lean.expected.out b/tests/lean/771.lean.expected.out new file mode 100644 index 000000000..2d64f2b48 --- /dev/null +++ b/tests/lean/771.lean.expected.out @@ -0,0 +1 @@ +771.lean:3:3: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly)