fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85

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

src/library/unifier.cpp

@@ -389,8 +389,20 @@ struct unifier_fn {
         m_next_assumption_idx = 0;
         m_next_cidx = 0;
         m_first     = true;
+        process_input_constraints(num_cs, cs);
+    }
+
+    void process_input_constraints(unsigned num_cs, constraint const * cs) {
+        // Input choice constraints may have ownership over a metavariable.
+        // So, we must first process them, to make sure the ownership table is initialized before
+        // we solve the remaining constraints
         for (unsigned i = 0; i < num_cs; i++) {
-            process_constraint(cs[i]);
+            if (cs[i].kind() == constraint_kind::Choice)
+                preprocess_choice_constraint(cs[i]);
+        }
+        for (unsigned i = 0; i < num_cs; i++) {
+            if (cs[i].kind() != constraint_kind::Choice)
+                process_constraint(cs[i]);
         }
     }
 

tests/lean/uni_bug1.lean

@@ -0,0 +1,9 @@
+import data.nat data.prod
+using nat prod
+
+variable R : nat → nat → Prop
+variable f (a b : nat) (H : R a b) : nat
+axiom Rtrue (a b : nat) : R a b
+
+
+check f 1 0 (Rtrue (pr1 (pair 1 0)) 0)

tests/lean/uni_bug1.lean.expected.out

@@ -0,0 +1,2 @@
+uni_bug1.lean:2:0: warning: imported file uses 'sorry'
+f 1 0 (Rtrue (pr1 (pair 1 0)) 0) : nat