feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2.

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

src/library/unifier.cpp

@@ -1581,12 +1581,51 @@ struct unifier_fn {
         return try_level_eq_zero(rhs, lhs, j);
     }
 
+    /** \brief Try to solve constraints of the form
+              (?m1 =?= max ?m2 ?m3)
+              (?m1 =?= max ?m2 ?m3)
+        by assigning ?m1 =?= ?m2 and ?m1 =?= ?m3
+
+        \remark we may miss solutions.
+    */
+    status try_merge_max_core(level const & lhs, level const & rhs, justification const & j) {
+        level m1 = lhs;
+        level m2, m3;
+        if (is_max(rhs)) {
+            m2 = max_lhs(rhs);
+            m3 = max_rhs(rhs);
+        } else if (is_imax(rhs)) {
+            m2 = imax_lhs(rhs);
+            m3 = imax_rhs(rhs);
+        } else {
+            return Continue;
+        }
+        if (process_constraint(mk_level_eq_cnstr(m1, m2, j)) &&
+            process_constraint(mk_level_eq_cnstr(m1, m3, j)))
+            return Solved;
+        else
+            return Failed;
+    }
+
+    /** \see try_merge_max_core */
+    status try_merge_max(constraint const & c) {
+        lean_assert(is_level_eq_cnstr(c));
+        level const & lhs = cnstr_lhs_level(c);
+        level const & rhs = cnstr_rhs_level(c);
+        justification const & j = c.get_justification();
+        status st = try_merge_max_core(lhs, rhs, j);
+        if (st != Continue) return st;
+        return try_merge_max_core(rhs, lhs, j);
+    }
+
     /** \brief Process the next constraint in the constraint queue m_cnstrs */
     bool process_next() {
         lean_assert(!m_cnstrs.empty());
         lean_assert(!m_tc[0]->next_cnstr());
         lean_assert(!m_tc[1]->next_cnstr());
-        constraint c = m_cnstrs.min()->first;
+        auto const * p = m_cnstrs.min();
+        unsigned cidx  = p->second;
+        constraint c   = p->first;
         m_cnstrs.erase_min();
         if (is_choice_cnstr(c)) {
             return process_choice_constraint(c);
@@ -1600,10 +1639,14 @@ struct unifier_fn {
                 if (modified)
                     return process_constraint(c);
                 status st = try_level_eq_zero(c);
-                if (st != Continue)
-                    return st == Solved;
-                else
-                    return process_plugin_constraint(c);
+                if (st != Continue) return st == Solved;
+                if (cidx < get_group_first_index(cnstr_group::FlexFlex)) {
+                    add_cnstr(c, cnstr_group::FlexFlex);
+                    return true;
+                }
+                st = try_merge_max(c);
+                if (st != Continue) return st == Solved;
+                return process_plugin_constraint(c);
             } else {
                 lean_assert(is_eq_cnstr(c));
                 if (is_delta_cnstr(c)) {

tests/lean/run/univ_bug1.lean

@@ -0,0 +1,26 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic data.nat
+using nat
+
+namespace simp
+-- set_option pp.universes true
+-- set_option pp.implicit true
+
+-- first define a class of homogeneous equality
+inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+| mk : t1 = t2 → simplifies_to t1 t2
+
+theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
+simplifies_to_rec (λx, x) C
+
+theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
+simplifies_to_rec (λx, x) C
+
+theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
+   (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
+mk (congr (get_eq C1) (get_eq C2))