fix(library/unifier): use depth-first search strategy for solving class-instance constraints

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

src/frontends/lean/elaborator.cpp

@@ -637,7 +637,7 @@ public:
                                                                        j, ignore_failure, m_relax_main_opaque));
             }
         };
-        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::DelayedChoice2), false, j, m_relax_main_opaque));
+        add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance), false, j, m_relax_main_opaque));
         return m;
     }
 
@@ -762,7 +762,7 @@ public:
         auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) {
             // Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap
             // for delaying coercions.
-            if (is_meta(new_d_type) && delay_factor < to_delay_factor(cnstr_group::DelayedChoice1)) {
+            if (is_meta(new_d_type) && delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) {
                 // The type is still unknown, delay the constraint even more.
                 return lazy_list<constraints>(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1)));
             } else {

src/library/unifier.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <memory>
 #include <vector>
+#include <limits>
 #include "util/interrupt.h"
 #include "util/luaref.h"
 #include "util/lazy_list_fn.h"
@@ -212,6 +213,15 @@ static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g
 static unsigned get_group_first_index(cnstr_group g) {
     return g_cnstr_group_first_index[static_cast<unsigned>(g)];
 }
+static unsigned get_group_last_index(cnstr_group g) {
+    unsigned g_idx = static_cast<unsigned>(g);
+    if (g_idx + 1 < g_num_groups) {
+        lean_assert(g_cnstr_group_first_index[g_idx+1] != 0);
+        return g_cnstr_group_first_index[g_idx+1]-1;
+    } else {
+        return std::numeric_limits<unsigned>::max();
+    }
+}
 static cnstr_group to_cnstr_group(unsigned d) {
     if (d >= g_num_groups)
         d = g_num_groups-1;
@@ -411,7 +421,13 @@ struct unifier_fn {
 
     /** \brief Add constraint to the constraint queue */
     unsigned add_cnstr(constraint const & c, cnstr_group g) {
-        unsigned cidx = m_next_cidx + get_group_first_index(g);
+        unsigned cidx;
+        if (g == cnstr_group::ClassInstance) {
+            // we use a stack discipline for solving class instances
+            cidx = get_group_last_index(g) - m_next_cidx;
+        } else {
+            cidx = m_next_cidx + get_group_first_index(g);
+        }
         m_cnstrs.insert(cnstr(c, cidx));
         m_next_cidx++;
         return cidx;
@@ -1845,8 +1861,8 @@ struct unifier_fn {
         lean_assert(!m_tc[1]->next_cnstr());
         auto const * p = m_cnstrs.min();
         unsigned cidx  = p->second;
-        if (!m_expensive && cidx >= get_group_first_index(cnstr_group::DelayedChoice2))
-            m_pattern = true; // use only higher-order (pattern) matching after we start processing MaxDelayed (aka class-instance constraints)
+        if (!m_expensive && cidx >= get_group_first_index(cnstr_group::ClassInstance))
+            m_pattern = true; // use only higher-order (pattern) matching after we start processing class-instance constraints
         constraint c   = p->first;
         // std::cout << "process_next: " << c << "\n";
         m_cnstrs.erase_min();

src/library/unifier.h

@@ -50,7 +50,7 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
                               bool relax_main_opaque, substitution const & s, options const & o);
 
 /**
-    The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice1, DelayedChoice2, FlexFlex, MaxDelayed
+    The unifier divides the constraints in 8 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed
 
     1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
        The are not even inserted in the constraint priority queue.
@@ -64,9 +64,9 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
        where elim is an eliminator/recursor and intro is an introduction/constructor.
        This constraints are delayed because after ?m is assigned we may be able to reduce them.
 
-    5) DelayedChoice1: for delayed choice constraints (we use this group for the maximally delayed coercions constraints).
+    5) DelayedChoice: for delayed choice constraints (we use this group for the maximally delayed coercions constraints).
 
-    6) DelayedChoice2: for delayed choice constraints (we use this group for class-instance).
+    6) ClassInstance: for delayed choice constraints (we use this group for class-instance).
 
     7) FlexFlex:  (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
        ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
@@ -74,7 +74,7 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
 
     8) MaxDelayed: maximally delayed constraint group
 */
-enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice1, DelayedChoice2, FlexFlex, MaxDelayed };
+enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed };
 inline unsigned to_delay_factor(cnstr_group g) { return static_cast<unsigned>(g); }
 
 class unifier_exception : public exception {

tests/lean/run/rel.lean

@@ -0,0 +1,38 @@
+import logic struc.relation
+using relation
+
+namespace is_equivalence
+
+  inductive class {T : Type} (R : T → T → Type) : Prop :=
+  | mk : is_reflexive.class R → is_symmetric.class R → is_transitive.class R → class R
+
+  theorem is_reflexive {T : Type} {R : T → T → Type} {C : class R} : is_reflexive.class R :=
+  class_rec (λx y z, x) C
+
+  theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric.class R :=
+  class_rec (λx y z, y) C
+
+  theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive.class R :=
+  class_rec (λx y z, z) C
+
+end is_equivalence
+
+instance is_equivalence.is_reflexive
+instance is_equivalence.is_symmetric
+instance is_equivalence.is_transitive
+
+theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
+iff_intro (take Hab, and_elim_right Hab) (take Hb, and_intro Ha Hb)
+
+theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
+gensubst.subst H1 H2
+
+theorem test2 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : Q ↔ (S ∧ Q) :=
+relation.operations.symm (and_inhabited_left Q H1)
+
+theorem test3 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
+gensubst.subst (test2 Q R S H3 H1) H3
+
+-- the composition of test2' and test3' fails
+theorem test4 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
+gensubst.subst (relation.operations.symm (and_inhabited_left Q H1)) H3