fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

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

src/library/unifier.cpp

@@ -662,7 +662,18 @@ struct unifier_fn {
         if (!m || is_meta(rhs))
             return Continue;
         expr bad_local;
-        switch (occurs_context_check(m_subst, rhs, *m, locals, bad_local)) {
+        auto status = occurs_context_check(m_subst, rhs, *m, locals, bad_local);
+        if (status == occurs_check_status::FailLocal || status == occurs_check_status::FailCircular) {
+            // Try to normalize rhs
+            // TODO(Leo): use a custom normalizer that uses reduction to solve just the failure.
+            // TODO(Leo): this code is using only whnf, we may fail to eliminate the failure.
+            // Example:  ?M := f (pr1 (pair 0 ?M))
+            constraint_seq cs;
+            expr rhs_whnf = whnf(rhs, relax, cs);
+            if (rhs != rhs_whnf && process_constraints(cs))
+                return process_metavar_eq(lhs, rhs_whnf, j, relax);
+        }
+        switch (status) {
         case occurs_check_status::FailLocal:
             set_conflict(mk_invalid_local_ctx_justification(lhs, rhs, j, bad_local));
             return Failed;

tests/lean/run/occurs_check_bug1.lean

@@ -0,0 +1,17 @@
+import logic data.nat data.prod
+
+using nat prod
+using decidable
+
+variable modulo (x : ℕ) (y : ℕ) : ℕ
+infixl `mod`:70 := modulo
+
+variable gcd_aux : ℕ × ℕ → ℕ
+
+definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)
+
+theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (decidable_eq (pr2 (pair x y)) 0) nat x (gcd y (x mod y)) :=
+sorry
+
+theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
+trans (gcd_def _ _) (if_neg (succ_ne_zero n) _ _)