From 4357c9196ed51ece15866919a2a77023c481e1bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Dec 2013 12:25:00 -0800 Subject: [PATCH] feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 60 +++++++++++- src/kernel/metavar.h | 17 +++- src/kernel/type_checker.cpp | 14 ++- src/library/elaborator/elaborator.cpp | 44 ++++++--- src/library/type_inferer.cpp | 6 +- src/tests/kernel/metavar.cpp | 71 ++++++++------ tests/lean/elab1.lean.expected.out | 86 ++++++++--------- tests/lean/lua15.lean.expected.out | 124 ++++++++++++------------- tests/lean/overload2.lean.expected.out | 90 +++++++++--------- 9 files changed, 295 insertions(+), 217 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index de18ea262..70e6c3ddf 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -159,19 +159,69 @@ bool metavar_env_cell::is_assigned(expr const & m) const { return is_assigned(metavar_name(m)); } -void metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) { +bool metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) { lean_assert(!is_assigned(m)); inc_timestamp(); + justification jst2 = jst; + buffer jsts; + expr t2 = instantiate_metavars(t, jsts); + if (!jsts.empty()) { + jst2 = justification(new normalize_assignment_justification(get_context(m), t, jst, + jsts.size(), jsts.data())); + } + unsigned ctx_size = get_context_size(m); + if (has_metavar(t2)) { + bool failed = false; + // Make sure the contexts of the metavariables occurring in \c t2 are + // not too big. + for_each(t2, [&](expr const & e, unsigned offset) { + if (is_metavar(e)) { + lean_assert(!is_assigned(e)); + unsigned range = free_var_range(e, metavar_env(this)); + if (range > ctx_size + offset) { + unsigned extra = range - ctx_size - offset; + auto it2 = m_metavar_data.find(metavar_name(e)); + if (it2 == nullptr) { + failed = true; + } else { + unsigned e_ctx_size = it2->m_context.size(); + if (e_ctx_size < extra) { + failed = true; + } else { + it2->m_context = it2->m_context.remove(e_ctx_size - extra, extra); + lean_assert(free_var_range(e, metavar_env(this)) == ctx_size + offset); + } + } + } + } + return true; + }); + if (failed) + return false; + } + if (free_var_range(t2, metavar_env(this)) > ctx_size) + return false; auto it = m_metavar_data.find(m); lean_assert(it); - it->m_subst = t; - it->m_justification = jst; + it->m_subst = t2; + it->m_justification = jst2; + return true; } -void metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) { +bool metavar_env_cell::assign(name const & m, expr const & t) { + justification j; + return assign(m, t, j); +} + +bool metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) { lean_assert(is_metavar(m)); lean_assert(!has_local_context(m)); - assign(metavar_name(m), t, j); + return assign(metavar_name(m), t, j); +} + +bool metavar_env_cell::assign(expr const & m, expr const & t) { + justification j; + return assign(m, t, j); } expr apply_local_context(expr const & a, local_context const & lctx, optional const & menv) { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 7bb25c01a..9f6b9c143 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -77,6 +77,9 @@ public: context get_context(expr const & m) const; context get_context(name const & m) const; + unsigned get_context_size(expr const & m) const { return get_context(m).size(); } + unsigned get_context_size(name const & m) const { return get_context(m).size(); } + /** \brief Return the type of the given metavariable. \pre is_metavar(m) @@ -126,17 +129,27 @@ public: \brief Assign metavariable named \c m. \pre !is_assigned(m) + + \remark The method returns false if the assignment cannot be performed + because \c t contain free variables that are not available in the context + associated with \c m. */ - void assign(name const & m, expr const & t, justification const & j = justification()); + bool assign(name const & m, expr const & t, justification const & j); + bool assign(name const & m, expr const & t); /** \brief Assign metavariable \c m to \c t. + \remark The method returns false if the assignment cannot be performed + because \c t contain free variables that are not available in the context + associated with \c m. + \pre is_metavar(m) \pre !has_meta_context(m) \pre !is_assigned(m) */ - void assign(expr const & m, expr const & t, justification const & j = justification()); + bool assign(expr const & m, expr const & t, justification const & j); + bool assign(expr const & m, expr const & t); /** \brief Return the substitution associated with the given metavariable diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 647265936..3a93d949d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -34,6 +34,14 @@ class type_checker::imp { return ro_environment(m_env); } + expr lift_free_vars(expr const & e, unsigned s, unsigned d) { + return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); + } + + expr lift_free_vars(expr const & e, unsigned d) { + return ::lean::lift_free_vars(e, d, m_menv.to_some_menv()); + } + expr normalize(expr const & e, context const & ctx) { return m_normalizer(e, ctx); } @@ -46,10 +54,10 @@ class type_checker::imp { return r; if (has_metavar(r) && m_menv && m_uc) { // Create two fresh variables A and B, - // and assign r == (Pi(x : A), B x) + // and assign r == (Pi(x : A), B) expr A = m_menv->mk_metavar(ctx); - expr B = m_menv->mk_metavar(ctx); - expr p = mk_pi(g_x_name, A, B(Var(0))); + expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); + expr p = mk_pi(g_x_name, A, B); justification jst = mk_function_expected_justification(ctx, s); m_uc->push_back(mk_eq_constraint(ctx, r, p, jst)); return p; diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index adcf0aab3..d705af5e4 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -163,10 +163,15 @@ class elaborator::imp { return mk_assumption_justification(id); } + void push_front(cnstr_queue & q, unification_constraint const & c) { + // std::cout << "PUSHING: "; display(std::cout, c); std::cout << "\n"; + q.push_front(c); + } + /** \brief Add given constraint to the front of the current constraint queue */ void push_front(unification_constraint const & c) { reset_quota(); - m_state.m_queue.push_front(c); + push_front(m_state.m_queue, c); } /** \brief Add given constraint to the end of the current constraint queue */ @@ -280,9 +285,9 @@ class elaborator::imp { */ void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { if (is_eq) - q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_jst)); + push_front(q, mk_eq_constraint(new_ctx, new_a, new_b, new_jst)); else - q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_jst)); + push_front(q, mk_convertible_constraint(new_ctx, new_a, new_b, new_jst)); } /** @@ -349,13 +354,18 @@ class elaborator::imp { /** \brief Assign \c v to \c m with justification \c tr in the current state. */ - void assign(expr const & m, expr const & v, unification_constraint const & c) { + bool assign(expr const & m, expr const & v, unification_constraint const & c, bool is_lhs) { lean_assert(is_metavar(m)); + if (instantiate_metavars(!is_lhs, v, c)) // make sure v does not have assigned metavars + return true; reset_quota(); context const & ctx = get_context(c); justification jst(new assignment_justification(c)); metavar_env const & menv = m_state.m_menv; - menv->assign(m, v, jst); + if (!menv->assign(m, v, jst)) { + m_conflict = justification(new unification_failure_justification(c)); + return false; + } if (menv->has_type(m)) { buffer ucs; expr tv = m_type_inferer(v, ctx, menv, ucs); @@ -364,6 +374,7 @@ class elaborator::imp { justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst)); push_front(mk_convertible_constraint(ctx, tv, menv->get_type(m), new_jst)); } + return true; } bool process(unification_constraint const & c) { @@ -414,8 +425,7 @@ class elaborator::imp { // or b is a proposition. // It is important to handle propositions since we don't want to normalize them. // The normalization process destroys the structure of the proposition. - assign(a, b, c); - return Processed; + return assign(a, b, c, is_lhs) ? Processed : Failed; } } else { local_entry const & me = head(metavar_lctx(a)); @@ -742,7 +752,10 @@ class elaborator::imp { unsigned num_a = num_args(a); buffer arg_types; buffer ucs; - context h_ctx = ctx; // context for new fresh metavariables used in the imitation step + // h_ctx is the context for new fresh metavariables used in the imitation step + // Since the imitation is going to be assigned to f_a, its context must + // be the context of f_a + the imitation arguments + context h_ctx = menv->get_context(metavar_name(f_a)); for (unsigned i = 1; i < num_a; i++) { arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs)); for (auto uc : ucs) @@ -821,7 +834,9 @@ class elaborator::imp { for further details. */ bool process_meta_app(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c, bool flex_flex = false) { - if (is_meta_app(a) && (flex_flex || !is_meta_app(b))) { + if (is_meta_app(a) && + (flex_flex || !is_meta_app(b)) && + (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) { std::unique_ptr new_cs(new generic_case_split(c, m_state)); process_meta_app_core(new_cs, a, b, is_lhs, c); if (flex_flex && is_meta_app(b)) @@ -853,7 +868,8 @@ class elaborator::imp { Case 2) imitate b */ bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { - if (is_metavar_inst(a) && !is_metavar_inst(b) && !is_meta_app(b)) { + if (is_metavar_inst(a) && !is_metavar_inst(b) && !is_meta_app(b) && + (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) { context const & ctx = get_context(c); local_context lctx = metavar_lctx(a); unsigned i = head(lctx).s(); @@ -963,7 +979,7 @@ class elaborator::imp { bool is_lower(unification_constraint const & c) { return is_convertible(c) && - is_metavar(convertible_to(c)) && + (is_metavar(convertible_to(c)) || is_meta_app(convertible_to(c))) && (is_bool(convertible_from(c)) || is_type(convertible_from(c))); } @@ -1115,14 +1131,12 @@ class elaborator::imp { if (!is_type(b) && !is_meta(b) && is_metavar(a) && !is_assigned(a) && !has_local_context(a)) { // We can assign a <- b at this point IF b is not (Type lvl) or Metavariable lean_assert(!has_metavar(b, a)); - assign(a, b, c); - return true; + return assign(a, b, c, true); } if (!is_type(a) && !is_meta(a) && a != Bool && is_metavar(b) && !is_assigned(b) && !has_local_context(b)) { // We can assign b <- a at this point IF a is not (Type lvl) or Metavariable or Bool. lean_assert(!has_metavar(a, b)); - assign(b, a, c); - return true; + return assign(b, a, c, false); } } diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index de8fd2ead..01345a618 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -65,10 +65,10 @@ class type_inferer::imp { t = abst_body(t); } else if (has_metavar(t) && m_menv && m_uc) { // Create two fresh variables A and B, - // and assign r == (Pi(x : A), B x) + // and assign r == (Pi(x : A), B) expr A = m_menv->mk_metavar(ctx); - expr B = m_menv->mk_metavar(ctx); - expr p = mk_pi(g_x_name, A, B(Var(0))); + expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); + expr p = mk_pi(g_x_name, A, B); justification jst = mk_function_expected_justification(ctx, e); m_uc->push_back(mk_eq_constraint(ctx, t, p, jst)); t = abst_body(p); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index a779c2f42..002aabeda 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -71,8 +71,9 @@ static void tst2() { expr g = Const("g"); expr h = Const("h"); expr a = Const("a"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}})); + expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}})); // move m1 to a different context, and store new metavariable + context in m11 std::cout << "---------------------\n"; expr m11 = add_inst(m1, 0, f(a, m2)); @@ -92,7 +93,7 @@ static void tst3() { expr a = Const("a"); expr x = Const("x"); expr T = Const("T"); - expr m1 = menv->mk_metavar(); + expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}})); expr F = Fun({x, T}, f(m1, x)); menv->assign(m1, h(Var(0), Var(2))); std::cout << instantiate(abst_body(F), g(a)) << "\n"; @@ -108,7 +109,8 @@ static void tst4() { expr g = Const("g"); expr h = Const("h"); expr a = Const("a"); - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}})); expr F = f(m1, Var(2)); menv->assign(m1, h(Var(1))); std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n"; @@ -128,8 +130,9 @@ static void tst6() { expr g = Const("g"); expr h = Const("h"); metavar_env menv; - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); + expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y))))); expr r = instantiate(t, g(m1, m2)); std::cout << r << std::endl; @@ -147,7 +150,8 @@ static void tst7() { expr g = Const("g"); expr a = Const("a"); metavar_env menv; - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x", T}})); expr t = f(m1, Var(0)); expr r = instantiate(t, a); menv->assign(m1, g(Var(0))); @@ -161,7 +165,8 @@ static void tst8() { expr g = Const("g"); expr a = Const("a"); metavar_env menv; - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); expr t = f(m1, Var(0), Var(2)); expr r = instantiate(t, a); menv->assign(m1, g(Var(0), Var(1))); @@ -175,7 +180,8 @@ static void tst9() { expr g = Const("g"); expr a = Const("a"); metavar_env menv; - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); expr t = f(m1, Var(1), Var(2)); expr r = lift_free_vars(t, 1, 2); std::cout << r << std::endl; @@ -196,8 +202,9 @@ static void tst10() { expr g = Const("g"); expr h = Const("h"); metavar_env menv; - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); + expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y))))); expr r = instantiate(t, g(m1)); std::cout << r << std::endl; @@ -224,7 +231,8 @@ static void tst11() { static void tst12() { metavar_env menv; - expr m = menv->mk_metavar(); + expr T = Const("T"); + expr m = menv->mk_metavar(context({{"x1", T}, {"x2", T}})); expr f = Const("f"); std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n"; std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n"; @@ -233,7 +241,8 @@ static void tst12() { static void tst13() { environment env; metavar_env menv; - expr m = menv->mk_metavar(); + expr T = Const("T"); + expr m = menv->mk_metavar(context({{"x", T}})); env->add_var("N", Type()); expr N = Const("N"); env->add_var("f", N >> N); @@ -253,8 +262,9 @@ static void tst13() { static void tst14() { environment env; metavar_env menv; - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}})); + expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}})); expr N = Const("N"); expr f = Const("f"); expr h = Const("h"); @@ -288,7 +298,8 @@ static void tst15() { environment env; metavar_env menv; normalizer norm(env); - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}})); expr f = Const("f"); expr x = Const("x"); expr y = Const("y"); @@ -311,7 +322,8 @@ static void tst16() { normalizer norm(env); context ctx; ctx = extend(ctx, "w", Type()); - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}})); expr f = Const("f"); expr x = Const("x"); expr y = Const("y"); @@ -334,7 +346,8 @@ static void tst17() { ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w3", Type()); ctx = extend(ctx, "w4", Type()); - expr m1 = menv->mk_metavar(); + expr T = Const("T"); + expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}})); expr f = Const("f"); expr x = Const("x"); expr y = Const("y"); @@ -379,7 +392,7 @@ static void tst18() { env->add_var("g", N >> N); env->add_var("h", N >> (N >> N)); expr m1 = menv->mk_metavar(context({{"z", Type()}, {"f", N >> N}, {"y", Type()}})); - expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}})); + expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}, {"x1", N}})); expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N)); std::cout << norm(F, ctx) << "\n"; metavar_env menv2 = menv.copy(); @@ -400,11 +413,11 @@ static void tst19() { context ctx; ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w2", Type()); - expr m1 = menv->mk_metavar(); - expr x = Const("x"); - expr y = Const("y"); - expr N = Const("N"); - expr F = Fun({{N, Type()}, {x, N}, {y, N}}, m1); + expr x = Const("x"); + expr y = Const("y"); + expr N = Const("N"); + expr m1 = menv->mk_metavar(context({{"N", Type()}, {"x", N}, {"y", N}})); + expr F = Fun({{N, Type()}, {x, N}, {y, N}}, m1); std::cout << norm(F) << "\n"; std::cout << norm(F, ctx) << "\n"; lean_assert(norm(F) == F); @@ -418,13 +431,13 @@ static void tst20() { context ctx; ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w2", Type()); - expr m1 = menv->mk_metavar(); expr x = Const("x"); expr y = Const("y"); expr z = Const("z"); expr N = Const("N"); expr a = Const("a"); expr b = Const("b"); + expr m1 = menv->mk_metavar(context({{"x", N}, {"y", N}, {"z", N}, {"x", N}, {"y", N}})); env->add_var("N", Type()); env->add_var("a", N); env->add_var("b", N); @@ -588,10 +601,10 @@ static void tst27() { env->add_var("a", Int); env->add_var("b", Real); expr T1 = menv->mk_metavar(); - expr T2 = menv->mk_metavar(); - expr A1 = menv->mk_metavar(); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); + expr T2 = menv->mk_metavar(context({{"x", T1}})); + expr A1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}})); + expr m1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}})); + expr m2 = menv->mk_metavar(context({{"x", T1}, {"y", T2}})); expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b)); std::cout << F << "\n"; std::cout << checker.infer_type(F, context(), menv, up) << "\n"; diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 070159bf3..109e6c336 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -18,7 +18,7 @@ Failed to solve Assignment ⊢ ℕ ≺ ?M::0 Substitution - ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 + ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: @@ -26,21 +26,19 @@ Failed to solve ?M::1 10 ⊤ Assignment - x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M::5 + x : ℕ ⊢ ℕ ≈ ?M::5 Destruct/Decompose - x : ℕ ⊢ ℕ ≈ ?M::5 x - Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 x - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℕ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ λ x : ℕ, x - Assumption 0 + ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 + Function expected at + ?M::1 10 + Assignment + ⊢ ℕ → ℕ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ λ x : ℕ, x + Assumption 0 Failed to solve ⊢ Bool ≺ ℤ Substitution @@ -54,7 +52,7 @@ Failed to solve Assignment ⊢ ℤ ≺ ?M::0 Substitution - ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 + ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: @@ -62,21 +60,19 @@ Failed to solve ?M::1 10 ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M::5 + _ : ℕ ⊢ ℤ ≈ ?M::5 Destruct/Decompose - _ : ℕ ⊢ ℤ ≈ ?M::5 _ - Destruct/Decompose - ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 x - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℤ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ nat_to_int - Assumption 1 + ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 + Function expected at + ?M::1 10 + Assignment + ⊢ ℕ → ℤ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ nat_to_int + Assumption 1 Failed to solve ⊢ Bool ≺ ℝ Substitution @@ -90,7 +86,7 @@ Failed to solve Assignment ⊢ ℝ ≺ ?M::0 Substitution - ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 + ⊢ ?M::5[inst:0 (10)] ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: @@ -98,26 +94,24 @@ Failed to solve ?M::1 10 ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M::5 + _ : ℕ ⊢ ℝ ≈ ?M::5 Destruct/Decompose - _ : ℕ ⊢ ℝ ≈ ?M::5 _ - Destruct/Decompose - ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 x - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x - Function expected at - ?M::1 10 - Assignment - ⊢ ℕ → ℝ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ nat_to_real - Assumption 2 + ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 + Function expected at + ?M::1 10 + Assignment + ⊢ ℕ → ℝ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ nat_to_real + Assumption 2 Assumed: g Error (line: 7, pos: 8) unexpected metavariable occurrence Assumed: h Failed to solve -x : ?M::0, A : Type ⊢ ?M::0[lift:0:2] ≺ A +x : ?M::0, A : Type ⊢ ?M::0 ≺ A (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of h with arguments: diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out index 94a771a32..7d34c61b8 100644 --- a/tests/lean/lua15.lean.expected.out +++ b/tests/lean/lua15.lean.expected.out @@ -17,34 +17,32 @@ Failed to solve Substitution ⊢ ℤ ≺ ?M::6 Substitution - ⊢ (?M::5[inst:0 i]) i ≺ ?M::6 + ⊢ ?M::5[inst:0 i] ≺ ?M::6 Type of argument 1 must be convertible to the expected type in the application of ?M::0 with arguments: ?M::1 i p Assignment - x : ℤ ⊢ λ x : ℤ, ℤ ≈ ?M::5 + x : ℤ ⊢ ℤ ≈ ?M::5 Destruct/Decompose - x : ℤ ⊢ ℤ ≈ ?M::5 x - Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 x - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x - Function expected at - ?M::1 i - Assignment - ⊢ ℤ → ℤ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ λ x : ℤ, x - Assumption 1 + ⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 + Function expected at + ?M::1 i + Assignment + ⊢ ℤ → ℤ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ λ x : ℤ, x + Assumption 1 Assignment ⊢ ℕ ≈ ?M::6 Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 Function expected at ?M::0 (?M::1 i) p Assignment @@ -58,34 +56,32 @@ Failed to solve Substitution ⊢ ℝ ≺ ?M::6 Substitution - ⊢ (?M::5[inst:0 i]) i ≺ ?M::6 + ⊢ ?M::5[inst:0 i] ≺ ?M::6 Type of argument 1 must be convertible to the expected type in the application of ?M::0 with arguments: ?M::1 i p Assignment - _ : ℤ ⊢ λ x : ℤ, ℝ ≈ ?M::5 + _ : ℤ ⊢ ℝ ≈ ?M::5 Destruct/Decompose - _ : ℤ ⊢ ℝ ≈ ?M::5 _ - Destruct/Decompose - ⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5 x - Substitution - ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x - Function expected at - ?M::1 i - Assignment - ⊢ ℤ → ℝ ≺ ?M::3 - Propagate type, ?M::1 : ?M::3 - Assignment - ⊢ ?M::1 ≈ int_to_real - Assumption 2 + ⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5 + Substitution + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 + Function expected at + ?M::1 i + Assignment + ⊢ ℤ → ℝ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 + Assignment + ⊢ ?M::1 ≈ int_to_real + Assumption 2 Assignment ⊢ ℕ ≈ ?M::6 Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 Function expected at ?M::0 (?M::1 i) p Assignment @@ -106,27 +102,25 @@ Failed to solve Assignment ⊢ ℤ ≈ ?M::8 Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x + ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 Substitution - ⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x + ⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9 Function expected at ?M::0 (?M::1 i) p Assignment - _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7 + _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 Destruct/Decompose - _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _ - Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x - Function expected at - ?M::0 (?M::1 i) p - Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Int::add - Assumption 3 + ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℤ → ℤ → ℤ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Int::add + Assumption 3 Failed to solve ⊢ Bool ≺ ℝ Substitution @@ -139,24 +133,22 @@ Failed to solve Assignment ⊢ ℝ ≈ ?M::8 Destruct/Decompose - ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x + ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 Substitution - ⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x + ⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9 Function expected at ?M::0 (?M::1 i) p Assignment - _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7 + _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 Destruct/Decompose - _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _ - Destruct/Decompose - ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x - Function expected at - ?M::0 (?M::1 i) p - Assignment - ⊢ ℝ → ℝ → ℝ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Real::add - Assumption 5 + ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + Function expected at + ?M::0 (?M::1 i) p + Assignment + ⊢ ℝ → ℝ → ℝ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Real::add + Assumption 5 diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index 2d47031cd..7c3d840df 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -16,27 +16,25 @@ Failed to solve Assignment ⊢ ℕ ≈ ?M::8 Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 x + ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 Substitution - ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x + ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 (line: 1: pos: 10) Function expected at ?M::0 (?M::1 1) ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M::7 + _ : ℕ ⊢ ℕ → ℕ ≈ ?M::7 Destruct/Decompose - _ : ℕ ⊢ ℕ → ℕ ≈ ?M::7 _ - Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x - (line: 1: pos: 10) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Nat::add - Assumption 0 + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + (line: 1: pos: 10) Function expected at + ?M::0 (?M::1 1) ⊤ + Assignment + ⊢ ℕ → ℕ → ℕ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Nat::add + Assumption 0 Failed to solve ⊢ Bool ≺ ℤ Substitution @@ -49,27 +47,25 @@ Failed to solve Assignment ⊢ ℤ ≈ ?M::8 Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x + ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 Substitution - ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x + ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 (line: 1: pos: 10) Function expected at ?M::0 (?M::1 1) ⊤ Assignment - _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7 + _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 Destruct/Decompose - _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _ - Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x - (line: 1: pos: 10) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Int::add - Assumption 2 + ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + (line: 1: pos: 10) Function expected at + ?M::0 (?M::1 1) ⊤ + Assignment + ⊢ ℤ → ℤ → ℤ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Int::add + Assumption 2 Failed to solve ⊢ Bool ≺ ℝ Substitution @@ -82,27 +78,25 @@ Failed to solve Assignment ⊢ ℝ ≈ ?M::8 Destruct/Decompose - ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x + ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 Substitution - ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x + ⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9 (line: 1: pos: 10) Function expected at ?M::0 (?M::1 1) ⊤ Assignment - _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7 + _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 Destruct/Decompose - _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _ - Destruct/Decompose - ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x - Substitution - ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x - (line: 1: pos: 10) Function expected at - ?M::0 (?M::1 1) ⊤ - Assignment - ⊢ ℝ → ℝ → ℝ ≺ ?M::2 - Propagate type, ?M::0 : ?M::2 - Assignment - ⊢ ?M::0 ≈ Real::add - Assumption 5 + ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 + Substitution + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 + (line: 1: pos: 10) Function expected at + ?M::0 (?M::1 1) ⊤ + Assignment + ⊢ ℝ → ℝ → ℝ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 + Assignment + ⊢ ?M::0 ≈ Real::add + Assumption 5 Assumed: R Assumed: T Assumed: r2t