fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/elaborator.cpp

@@ -615,7 +615,7 @@ public:
                                                                        ignore_failure, m_relax_main_opaque));
             }
         };
-        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j, m_relax_main_opaque));
+        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), false, j, m_relax_main_opaque));
         return m;
     }
 
@@ -657,7 +657,7 @@ public:
             return choose(std::make_shared<choice_expr_elaborator>(*this, mvar, e, ctx, s, relax));
         };
         justification j = mk_justification("none of the overloads is applicable", some_expr(e));
-        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j, m_relax_main_opaque));
+        add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque));
         return m;
     }
 
@@ -733,7 +733,7 @@ public:
                 return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, r, justification(), relax)));
             }
         };
-        return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque);
+        return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, m_relax_main_opaque);
     }
 
     /** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */

src/kernel/constraint.cpp

@@ -33,9 +33,10 @@ struct choice_constraint_cell : public constraint_cell {
     expr      m_expr;
     choice_fn m_fn;
     unsigned  m_delay_factor;
-    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax):
+    bool      m_owner;
+    choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax):
         constraint_cell(constraint_kind::Choice, j, relax),
-        m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {}
+        m_expr(e), m_fn(fn), m_delay_factor(delay_factor), m_owner(owner) {}
 };
 
 void constraint_cell::dealloc() {
@@ -64,9 +65,9 @@ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const &
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
     return constraint(new level_constraint_cell(lhs, rhs, j));
 }
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque) {
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque) {
     lean_assert(is_meta(m));
-    return constraint(new choice_constraint_cell(m, fn, delay_factor, j, relax_main_opaque));
+    return constraint(new choice_constraint_cell(m, fn, delay_factor, owner, j, relax_main_opaque));
 }
 
 expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast<eq_constraint_cell*>(c.raw())->m_lhs; }
@@ -87,6 +88,9 @@ choice_fn const & cnstr_choice_fn(constraint const & c) {
 unsigned cnstr_delay_factor(constraint const & c) {
     lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor;
 }
+bool cnstr_is_owner(constraint const & c) {
+    lean_assert(is_choice_cnstr(c)); return static_cast<choice_constraint_cell*>(c.raw())->m_owner;
+}
 
 constraint update_justification(constraint const & c, justification const & j) {
     switch (c.kind()) {
@@ -95,7 +99,7 @@ constraint update_justification(constraint const & c, justification const & j) {
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
     case constraint_kind::Choice:
-        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j, relax_main_opaque(c));
+        return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), cnstr_is_owner(c), j, relax_main_opaque(c));
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }

src/kernel/constraint.h

@@ -67,8 +67,8 @@ public:
 
     friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
     friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j,
+    friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner,
-                                      bool relax_main_opaque);
+                                      justification const & j, bool relax_main_opaque);
 
     constraint_cell * raw() const { return m_ptr; }
 };
@@ -76,13 +76,21 @@ public:
 inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); }
 inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
 
-/**
+/** \brief Create a unification constraint lhs =?= rhs
-   \brief Create a unification constraint lhs =?= rhs
     If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent.
 */
 constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
-constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque);
+/** \brief Create a "choice" constraint m in fn(...), where fn produces a stream of possible solutions.
+    \c delay_factor allows to control when the constraint is processed by the elaborator, bigger == later.
+    If \c owner is true, then the elaborator should not assign the metavariable get_app_fn(m).
+    The variable will be assigned by the choice constraint, and the elaborator should just check whether a solution
+    produced by fn satisfies the other constraints or not.
+    \c j is a justification for the constraint.
+    If \c relax_main_opaque is true, then it signs that constraint was created in a context where
+    opaque constants of the main module can be treated as transparent.
+*/
+constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque);
 
 inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@@ -106,6 +114,8 @@ expr const & cnstr_expr(constraint const & c);
 choice_fn const & cnstr_choice_fn(constraint const & c);
 /** \brief Return the choice constraint delay factor */
 unsigned cnstr_delay_factor(constraint const & c);
+/** \brief Return true iff the given choice constraints owns the right to assign the metavariable in \c c. */
+bool cnstr_is_owner(constraint const & c);
 
 /** \brief Printer for debugging purposes */
 std::ostream & operator<<(std::ostream & out, constraint const & c);

src/library/kernel_bindings.cpp

@@ -1528,15 +1528,19 @@ static int mk_choice_cnstr(lua_State * L) {
     expr m           = to_expr(L, 1);
     choice_fn fn     = to_choice_fn(L, 2);
     if (nargs == 2)
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification(), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification(), false));
     else if (nargs == 3 && is_justification(L, 3))
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3), false));
     else if (nargs == 3)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification(), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification(), false));
     else if (nargs == 4)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification(), false));
+    else if (nargs == 5)
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
+                                                  to_justification(L, 5), false));
     else
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), lua_toboolean(L, 5)));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
+                                                  to_justification(L, 5), lua_toboolean(L, 6)));
 }
 
 static int constraint_expr(lua_State * L) {

src/library/unifier.cpp

@@ -211,10 +211,16 @@ unify_status unify_simple(substitution & s, constraint const & c) {
 
 static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
 static unsigned g_group_size = 1u << 29;
-static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
+constexpr unsigned g_num_groups = 6;
+static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size};
 static unsigned get_group_first_index(cnstr_group g) {
     return g_cnstr_group_first_index[static_cast<unsigned>(g)];
 }
+static cnstr_group to_cnstr_group(unsigned d) {
+    if (d >= g_num_groups)
+        d = g_num_groups-1;
+    return static_cast<cnstr_group>(d);
+}
 
 /** \brief Convert choice constraint delay factor to cnstr_group */
 cnstr_group get_choice_cnstr_group(constraint const & c) {
@@ -236,10 +242,12 @@ struct unifier_fn {
     typedef rb_tree<cnstr, cnstr_cmp> cnstr_set;
     typedef rb_tree<unsigned, unsigned_cmp> cnstr_idx_set;
     typedef rb_map<name, cnstr_idx_set, name_quick_cmp> name_to_cnstrs;
+    typedef rb_map<name, unsigned, name_quick_cmp> owned_map;
     typedef std::unique_ptr<type_checker> type_checker_ptr;
     environment      m_env;
     name_generator   m_ngen;
     substitution     m_subst;
+    owned_map        m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m
     unifier_plugin   m_plugin;
     type_checker_ptr m_tc[2];
     bool             m_use_exception; //!< True if we should throw an exception when there are no more solutions.
@@ -286,11 +294,12 @@ struct unifier_fn {
         substitution     m_subst;
         cnstr_set        m_cnstrs;
         name_to_cnstrs   m_mvar_occs;
+        owned_map        m_owned_map;
 
         /** \brief Save unifier's state */
         case_split(unifier_fn & u, justification const & j):
             m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs),
-            m_mvar_occs(u.m_mvar_occs) {
+            m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map) {
             u.m_next_assumption_idx++;
             u.m_tc[0]->push();
             u.m_tc[1]->push();
@@ -306,6 +315,7 @@ struct unifier_fn {
             u.m_subst     = m_subst;
             u.m_cnstrs    = m_cnstrs;
             u.m_mvar_occs = m_mvar_occs;
+            u.m_owned_map = m_owned_map;
             m_assumption_idx = u.m_next_assumption_idx;
             m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict);
             u.m_next_assumption_idx++;
@@ -608,12 +618,41 @@ struct unifier_fn {
         return Continue;
     }
 
+    /** \brief Return a delay factor if e is of the form (?m ...) and ?m is a metavariable owned by
+        a choice constraint. The delay factor is the delay of the choice constraint.
+        Return none otherwise. */
+    optional<unsigned> is_owned(expr const & e) {
+        expr const & m = get_app_fn(e);
+        if (!is_metavar(m))
+            return optional<unsigned>();
+        if (auto it = m_owned_map.find(mlocal_name(m)))
+            return optional<unsigned>(*it);
+        else
+            return optional<unsigned>();
+    }
+
+    /** \brief Applies previous method to the left and right hand sides of the equality constraint */
+    optional<unsigned> is_owned(constraint const & c) {
+        if (auto d = is_owned(cnstr_lhs_expr(c)))
+            return d;
+        else
+            return is_owned(cnstr_rhs_expr(c));
+    }
+
     /** \brief Process an equality constraints. */
     bool process_eq_constraint(constraint const & c) {
         lean_assert(is_eq_cnstr(c));
         // instantiate assigned metavariables
         status st = instantiate_eq_cnstr(c);
         if (st != Continue) return st == Solved;
+
+        if (auto d = is_owned(c)) {
+            // Metavariable in the constraint is owned by choice constraint.
+            // So, we postpone this constraint.
+            add_cnstr(c, to_cnstr_group(*d+1));
+            return true;
+        }
+
         st = process_eq_constraint_core(c);
         if (st != Continue) return st == Solved;
 
@@ -707,6 +746,17 @@ struct unifier_fn {
         return true;
     }
 
+    bool preprocess_choice_constraint(constraint const & c) {
+        if (cnstr_is_owner(c)) {
+            expr m = get_app_fn(cnstr_expr(c));
+            lean_assert(is_metavar(m));
+            m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c));
+        }
+        // Choice constraints are never considered easy.
+        add_cnstr(c, get_choice_cnstr_group(c));
+        return true;
+    }
+
     /**
         \brief Process the given constraint \c c. "Easy" constraints are solved, and the remaining ones
         are added to the constraint queue m_cnstrs. By "easy", see the methods
@@ -718,9 +768,7 @@ struct unifier_fn {
         check_system();
         switch (c.kind()) {
         case constraint_kind::Choice:
-            // Choice constraints are never considered easy.
+            return preprocess_choice_constraint(c);
-            add_cnstr(c, get_choice_cnstr_group(c));
-            return true;
         case constraint_kind::Eq:
             return process_eq_constraint(c);
         case constraint_kind::LevelEq:
@@ -878,6 +926,11 @@ struct unifier_fn {
         lean_assert(is_choice_cnstr(c));
         expr const &   m            = cnstr_expr(c);
         choice_fn const & fn        = cnstr_choice_fn(c);
+        if (cnstr_is_owner(c)) {
+            // choice will have a chance to assign m, so
+            // we remove the "barrier" that was preventing m from being assigned.
+            m_owned_map.erase(mlocal_name(get_app_fn(m)));
+        }
         expr m_type;
         bool relax = relax_main_opaque(c);
         try {

tests/lean/run/coercion_bug2.lean

@@ -0,0 +1,11 @@
+import nat
+using nat
+
+inductive list (T : Type) : Type :=
+| nil {} : list T
+| cons : T → list T → list T
+
+definition length {T : Type} : list T → nat := list_rec 0 (fun x l m, succ m)
+theorem length_nil {T : Type} : length (@nil T) = 0
+:= refl _
+