From 6cf73b51e2f59f923cea7066c0a888d52ac90963 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Aug 2014 17:56:18 -0700
Subject: [PATCH] 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               | 13 ++++++++++++-
 tests/lean/run/occurs_check_bug1.lean | 17 +++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/occurs_check_bug1.lean

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 117b3b4f2..bab982c76 100644
--- a/src/library/unifier.cpp
+++ b/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;
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
new file mode 100644
index 000000000..5f863e393
--- /dev/null
+++ b/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) _ _)