diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 2845aab650..ade2679220 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -32,6 +32,7 @@ Author: Leonardo de Moura #include "library/fun_info.h" #include "library/num.h" #include "library/quote.h" +#include "library/check.h" #ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH #define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 @@ -1923,18 +1924,42 @@ Now, we consider some workarounds/approximations. which is again type incorrect. - TODO(Leo): we address this issue by type checking the term after - abstraction AND for each metavariable that may contain a local constant - that depends on a term being abstracted, we create a fresh metavariable - with a smaller local context. In the example above, when we perform - the assignment + We can address the issue on the first example by type checking + the term after abstraction. This is not a significant performance + bottleneck because this case doesn't happen very often in practice + (262 times when compiling corelib on Jan 2018). The second example + is trickier, but it also occurs less frequently (8 times when compiling + corelib on Jan 2018, and all occurrences were in init/category when + we definy monads and auxiliary combinators for them). + We considered three options for the addressing the issue on the second example: - ?m_1 := (fun α'. id ?m_2[α := α']) + a) For each metavariable that may contain a local constant + that depends on a term being abstracted, we create a fresh metavariable + with a smaller local context. In the example above, when we perform + the assignment - we would also create a fresh ?m_3 with local context containing only (α : Type), - and assign + ?m_1 := (fun α'. id ?m_2[α := α']) - ?m_2 := ?m_3 + we would also create a fresh ?m_3 with local context containing only (α : Type), + and assign + + ?m_2 := ?m_3 + + This is an approximation, and it may reject valid assignments. + + b) If we find a metavariable with this kind of dependency, we just + fail and fallback to first-order unification. + + c) If we find a metavariable on the term after abstraction, we just + fail and fallback to first-order unification. + + The first two options are incomparable, each one of them can solve + problems where the other fails. The third one is weaker than the second, + but we didn't find any example in the corelib where the second option + applies. The first and third options are also incomparable. + + So, we decide to use the third option since it is the simplest to implement, + and all examples we have identified are in init/category. A3) `a_1 ... a_n` are not pairwise distinct (failed condition 1). We can approximate again, but the limitations are very similar to the previous one. @@ -2022,8 +2047,14 @@ bool type_context::process_assignment(expr const & m, expr const & v) { bool use_fo = false; /* if true, we use first-order unification */ bool add_locals = true; /* while true we copy args to locals */ /* in_ctx_locals is a subset of the local constants in `locals`. - See workaround A2. We use these locals to shrink the local context - of metavariables occuring in `v`. */ + See workaround A2. + + In principle, we only need one store one bit indicating + whether there is a locals in `locals` that is the local context + of the metavariable or not. This is all we need to implement + option c) in the workaround A2. + We store all occurrences because we may decide to implement options a) or b). + */ buffer in_ctx_locals; for (unsigned i = 0; i < args.size(); i++) { expr arg = args[i]; @@ -2087,8 +2118,10 @@ bool type_context::process_assignment(expr const & m, expr const & v) { if (use_fo) return process_assignment_fo_approx(mvar, args, new_v); - if (optional new_new_v = check_assignment(locals, mvar, new_v)) + if (optional new_new_v = check_assignment(locals, in_ctx_locals, mvar, new_v)) new_v = *new_new_v; + else if (approximate() && !args.empty()) + return process_assignment_fo_approx(mvar, args, new_v); else return false; @@ -2120,6 +2153,24 @@ bool type_context::process_assignment(expr const & m, expr const & v) { new_v = mk_lambda(locals, new_v); } + if (!in_ctx_locals.empty()) { + lean_assert(approximate()); + try { + /* We need to type check new_v because abstraction using `mk_lambda` may have produced + a type incorrect term. See discussion at A2. + + Remark: this test should not be a performance bottleneck. On Jan 2018, this check + had to be performed only 262 times when compiling corelib, and 823 times when + compiling mathlib. */ + ::lean::check(*this, new_v); + } catch (exception &) { + if (args.size() > 0) + return process_assignment_fo_approx(mvar, args, new_v); + else + return false; + } + } + /* check types */ try { expr t1 = infer(mvar); @@ -2230,12 +2281,13 @@ struct check_assignment_failed {}; struct check_assignment_fn : public replace_visitor { type_context & m_ctx; buffer const & m_locals; + buffer const & m_in_ctx_locals; expr const & m_mvar; optional m_mvar_decl; expr m_value; - check_assignment_fn(type_context & ctx, buffer const & locals, expr const & mvar): - m_ctx(ctx), m_locals(locals), m_mvar(mvar) { + check_assignment_fn(type_context & ctx, buffer const & locals, buffer const & in_ctx_locals, expr const & mvar): + m_ctx(ctx), m_locals(locals), m_in_ctx_locals(in_ctx_locals), m_mvar(mvar) { if (!m_ctx.in_tmp_mode()) { m_mvar_decl = m_ctx.m_mctx.get_metavar_decl(mvar); lean_assert(m_mvar_decl); @@ -2285,8 +2337,6 @@ struct check_assignment_fn : public replace_visitor { expr visit_meta_core(expr const & e, buffer const & delayed_locals) { if (auto v = m_ctx.get_assignment(e)) return visit(*v); - if (!m_ctx.is_mode_mvar(e)) return replace_visitor::visit_meta(e); - if (m_mvar == e) { /* mvar occurs in m_value */ lean_trace(name({"type_context", "is_def_eq_detail"}), @@ -2296,7 +2346,31 @@ struct check_assignment_fn : public replace_visitor { throw check_assignment_failed(); } + if (!m_ctx.is_mode_mvar(e)) { + if (!m_in_ctx_locals.empty()) { + /* + This code is reachable if we are in tmp mode and `e` is regular metavariable. + We just fail, and this is ok because we usually do not use + approximate unification/matching in tmp mode. + + Remark: this code was not reachable when compiling corelib on Jan 2018. + */ + throw check_assignment_failed(); + } + return replace_visitor::visit_meta(e); + } + if (m_ctx.in_tmp_mode()) { + if (!m_in_ctx_locals.empty()) { + /* In tmp mode, we (usually) do not use approximate unification/matching. + Moreover, m_in_ctx_locals is empty if !approximate(). + + Remark: all temporary metavariables share the same local context. + Then, if a local in `m_in_ctx_locals` is in the local context of `mvar`, + then it will also be in the local context of `e`. */ + throw check_assignment_failed(); + } + /* Recall that in tmp_mode all metavariables have the same local context. So, we don't need to check anything. In regular mode, we need to check condition 4 @@ -2318,6 +2392,12 @@ struct check_assignment_fn : public replace_visitor { local_context mvar_lctx = m_mvar_decl->get_context(); local_context e_lctx = e_decl->get_context(); + + if (!m_in_ctx_locals.empty()) { + /* We are using option c) described at workaround A2. */ + throw check_assignment_failed(); + } + if (is_subset_of(e_lctx, mvar_lctx, delayed_locals)) return e; @@ -2400,9 +2480,9 @@ struct check_assignment_fn : public replace_visitor { }; /* Auxiliary method for process_assignment */ -optional type_context::check_assignment(buffer const & locals, expr const & mvar, expr v) { +optional type_context::check_assignment(buffer const & locals, buffer const & in_ctx_locals, expr const & mvar, expr v) { try { - return some_expr(check_assignment_fn(*this, locals, mvar)(v)); + return some_expr(check_assignment_fn(*this, locals, in_ctx_locals, mvar)(v)); } catch (check_assignment_failed &) { return none_expr(); } diff --git a/src/library/type_context.h b/src/library/type_context.h index 0708c7bc64..ba5879e1ed 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -1060,7 +1060,7 @@ private: expr try_zeta(expr const & e); expr expand_let_decls(expr const & e); friend struct check_assignment_fn; - optional check_assignment(buffer const & locals, expr const & mvar, expr v); + optional check_assignment(buffer const & locals, buffer const & in_ctx_locals, expr const & mvar, expr v); bool process_assignment(expr const & m, expr const & v); bool process_assignment_fo_approx(expr const & mvar, buffer const & args, expr const & new_v); diff --git a/tests/lean/run/unify_approx_bug.lean b/tests/lean/run/unify_approx_bug.lean index 3263bb4ead..5d156ef15c 100644 --- a/tests/lean/run/unify_approx_bug.lean +++ b/tests/lean/run/unify_approx_bug.lean @@ -14,15 +14,15 @@ open tactic ?m := λ α', ((λ (α : Type) (a : α), α) α' a) -/ def ex1 (α : Type) (a : α) : Type → Type := -by +by do + fail_if_success (do mvar1 ← mk_meta_var `(Type → Type), alpha ← to_expr ```(α), t ← to_expr ```((λ (α : Type) (a : α), α) α a), unify (mvar1 alpha) t semireducible tt, -- should fail - exact mvar1) - <|> - (intros >> assumption) + exact mvar1), + intros, assumption /- Given metavariable ?m_1 and ?m_2 with local context @@ -34,17 +34,15 @@ by ?m_1 α =?= id ?m_2 ?m_2 =?= α - After processing the first constraint, we have + The first constraint is solved using first-order unification + because we cannot guarantee that the solution will be type correct + for every term we may assign to `?m_2` - ?m_1 := λ α', id ?m_2[α := α'] - ?m_2 := ?m_3 + ?m_1 := λ α', id ?m_2[α := α'] - where ?m_3 is a fresh metavariable with a local context - that does not contain `a`, since `a` depends on `α`. + So, we get `?m_2 := α`. - After processing the second constraint, we have - - ?m_3 := α + Remark: see option c) at workaround A2 described at type_context::process_assignment -/ def ex2 (α : Type) (a : α) : Type → Type := by do @@ -52,8 +50,8 @@ by do mvar2 ← mk_meta_var `(Type), alpha ← to_expr ```(α), t ← to_expr ```(id %%mvar2), - unify (mvar1 alpha) t semireducible tt, -- should create an auxiliary mvar and assign it to mvar2 - unify mvar2 alpha, -- the local context of the auxiliary declaration does not contain `a` + unify (mvar1 alpha) t semireducible tt, -- first-order unification is used here + unify mvar2 alpha, exact mvar1 /- @@ -66,20 +64,14 @@ by do ?m_1 α =?= id ?m_2 ?m_2 =?= ((λ (α : Type) (a : α), α) α a) - After processing the first constraint, we have - - ?m_1 := λ α', id ?m_2[α := α'] - ?m_2 := ?m_3 - - where ?m_3 is a fresh metavariable with a local context - that does not contain `a`, since `a` depends on `α`. - - When processing the second constraint, it fails - because it tries to assing `((λ (α : Type) (a : α), α) α a)` - to `?m_3`, but `a` is not in the context of `?m_3`. + Again, similarly to the previous example, we use + first-order unification to process the first constraint, + and we get `?m_2 := α`. The second constraint + is satisfied because `((λ (α : Type) (a : α), α) α a)` + is definitionally equal to `α`. -/ def ex3 (α : Type) (a : α) : Type → Type := -by (do +by do mvar1 ← mk_meta_var `(Type → Type), mvar2 ← mk_meta_var `(Type), alpha ← to_expr ```(α), @@ -87,11 +79,12 @@ by (do unify (mvar1 alpha) t semireducible tt, -- should create an auxiliary mvar and assign it to mvar2 t ← to_expr ```((λ (α : Type) (a : α), α) α a), unify mvar2 t semireducible tt, -- should fail `a` is not in the scope - exact mvar1) - <|> (intros >> assumption) + exact mvar1 def f (α : Type) (a : α) := α +constant f' (α : Type) (a : α) : Type + /- Given a metavariable ?m with local context @@ -106,15 +99,15 @@ def f (α : Type) (a : α) := α ?m := λ α', f α' a -/ def ex4 (α : Type) (a : α) : Type → Type := -by +by do + fail_if_success (do mvar1 ← mk_meta_var `(Type → Type), alpha ← to_expr ```(α), t ← to_expr ```(f α a), unify (mvar1 alpha) t semireducible tt, -- should fail - exact mvar1) - <|> - (intros >> assumption) + exact mvar1), + intros, assumption /- Given a metavariable ?m with local context @@ -138,6 +131,15 @@ by do unify (mvar1 alpha a) t semireducible tt, -- should work exact mvar1 +def ex5b (α : Type) (a : α) : Π A : Type, A → Type := +by do + mvar1 ← mk_meta_var `(Π A : Type, A → Type), + alpha ← to_expr ```(α), + a ← to_expr ```(a), + t ← to_expr ```(f' α a), + unify (mvar1 alpha a) t semireducible tt, -- should work + exact mvar1 + /- Given metavariable ?m_1 and ?m_2 with local context @@ -148,29 +150,46 @@ by do ?m_1 α =?= id ?m_2 ?m_2 =?= f α a - After processing the first constraint, we have - - ?m_1 := λ α', id ?m_2[α := α'] - ?m_2 := ?m_3 - - where ?m_3 is a fresh metavariable with a local context - that does not contain `a`, since `a` depends on `α`. - - When processing the second constraint, it fails - because it tries to assign `f α a` - to `?m_3`, but `a` is not in the context of `?m_3`. + The first constraint is solved using first-order unification. + See option c) at workaround A2 described at type_context::process_assignment. + Then, we get `?m_2 := α`. The second constraint succeeds + because `f α a` is definitionally equal to `α`. -/ def ex6 (α : Type) (a : α) : Type → Type := -by (do - mvar1 ← mk_meta_var `(Type → Type), +by do mvar1 ← mk_meta_var `(Type → Type), mvar2 ← mk_meta_var `(Type), alpha ← to_expr ```(α), t ← to_expr ```(id %%mvar2), - unify (mvar1 alpha) t semireducible tt, -- should create an auxiliary mvar and assign it to mvar2 + unify (mvar1 alpha) t semireducible tt, t ← to_expr ```(f α a), - unify mvar2 t semireducible tt, -- should fail `a` is not in the scope - exact mvar1) - <|> (intros >> assumption) + unify mvar2 t semireducible tt, + exact mvar1 + +/- + Given metavariable ?m_1 and ?m_2 with local context + + (α : Type) (a : α) + + then, the following unification constrains should be solved + + ?m_1 α =?= id ?m_2 + ?m_2 =?= f' α a + + Similar to previous example, but this one fails because + `f' α a` is not definitionally equal to `α`. +-/ +def ex6b (α : Type) (a : α) : Type → Type := +by do + fail_if_success + (do mvar1 ← mk_meta_var `(Type → Type), + mvar2 ← mk_meta_var `(Type), + alpha ← to_expr ```(α), + t ← to_expr ```(id %%mvar2), + unify (mvar1 alpha) t semireducible tt, + t ← to_expr ```(f' α a), + unify mvar2 t semireducible tt, + exact mvar1), + intros, assumption def g (α : Type) (a b : α) := α @@ -188,15 +207,15 @@ def g (α : Type) (a b : α) := α ?m := λ α', g α' a a -/ def ex7 (α : Type) (a : α) : Type → Type := -by +by do + fail_if_success (do mvar1 ← mk_meta_var `(Type → Type), alpha ← to_expr ```(α), t ← to_expr ```(g α a a), unify (mvar1 alpha) t semireducible tt, -- should fail - exact mvar1) - <|> - (intros >> assumption) + exact mvar1), + intros, assumption constant C (α : Type) (a : α) : Type @@ -217,16 +236,17 @@ constant C (α : Type) (a : α) : Type with type of (λ (α' : Type) (x' : C α' a), α') -/ def ex8 (α : Type) (a : α) (x : C α a) : Type := -by - (do - mvar_type ← to_expr ```(C α a → Type), - mvar_type ← to_expr ```(Type → %%mvar_type), - mvar1 ← mk_meta_var mvar_type, - alpha ← to_expr ```(α), - x ← to_expr ```(x), - unify (mvar1 alpha x) alpha semireducible tt, -- should fail - exact (mvar1 alpha x)) - <|> assumption +by do + fail_if_success + (do + mvar_type ← to_expr ```(C α a → Type), + mvar_type ← to_expr ```(Type → %%mvar_type), + mvar1 ← mk_meta_var mvar_type, + alpha ← to_expr ```(α), + x ← to_expr ```(x), + unify (mvar1 alpha x) alpha semireducible tt, -- should fail + exact (mvar1 alpha x)), + assumption /- Given a metavariable ?m with local context