fix(library/unifier): bug in unifier priority queue

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

src/library/unifier.cpp

@@ -1892,6 +1892,12 @@ struct unifier_fn {
                     return process_delta(c);
                 } else if (modified) {
                     return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
+                } else if (auto d = is_owned(c)) {
+                    // Metavariable in the constraint is owned by choice constraint.
+                    // choice constraint was postponed... since c was not modifed
+                    // So, we should postpone this one too.
+                    add_cnstr(c, to_cnstr_group(*d+1));
+                    return true;
                 } else if (is_flex_rigid(c)) {
                     return process_flex_rigid(c);
                 } else if (is_flex_flex(c)) {

tests/lean/interactive/test_single.sh

@@ -5,6 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
 fi
 ulimit -s unlimited
 LEAN=$1
+export LEAN_PATH=../../../library/standard:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else

tests/lean/run/coe7.lean

@@ -0,0 +1,11 @@
+import logic
+
+variable nat : Type.{1}
+variable int : Type.{1}
+variable of_nat : nat → int
+coercion of_nat
+
+theorem tst (n : nat) : n = n :=
+have H : true, from trivial,
+calc n    = n : refl _
+      ... = n : refl _