feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization

This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean

src/library/normalize.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/interrupt.h"
 #include "util/name_generator.h"
 #include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
@@ -14,7 +15,7 @@ namespace lean {
 class normalize_fn {
     type_checker   &                  m_tc;
     name_generator                    m_ngen;
-    std::function<bool(expr const &)> m_pred;
+    std::function<bool(expr const &)> m_pred;  // NOLINT
     bool                              m_save_cnstrs;
     constraint_seq                    m_cnstrs;
 
@@ -34,6 +35,7 @@ class normalize_fn {
     }
 
     expr normalize(expr e) {
+        check_system("normalize");
         if (!m_pred(e))
             return e;
         auto w = m_tc.whnf(e);
@@ -58,7 +60,7 @@ public:
         m_pred([](expr const &) { return true; }),
         m_save_cnstrs(save) {}
 
-    normalize_fn(type_checker & tc, std::function<bool(expr const &)> const & fn):
+    normalize_fn(type_checker & tc, std::function<bool(expr const &)> const & fn): // NOLINT
         m_tc(tc), m_ngen(m_tc.mk_ngen()),
         m_pred(fn) {}
 
@@ -101,7 +103,8 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs) {
     return r;
 }
 
-expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const &)> const & pred, constraint_seq & cs) {
+expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const &)> const & pred, // NOLINT
+               constraint_seq & cs) {
     normalize_fn fn(tc, pred);
     expr r = fn(e);
     cs += fn.get_cnstrs();

src/library/normalize.h

@@ -28,6 +28,6 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs);
 
     \remark A sub-expression is evaluated only if \c pred returns true.
 */
-expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred,
+expr normalize(type_checker & tc, expr const & e, std::function<bool(expr const&)> const & pred, // NOLINT
                constraint_seq & cs);
 }

src/library/unifier.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/error_msgs.h"
+#include "library/normalize.h"
 #include "library/occurs.h"
 #include "library/locals.h"
 #include "library/module.h"
@@ -726,13 +727,18 @@ struct unifier_fn {
         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);
+            auto is_target_fn = [&](expr const & e) {
+                if (status == occurs_check_status::FailLocal && occurs(bad_local, e))
+                    return true;
+                else if (status == occurs_check_status::FailCircular && occurs(*m, e))
+                    return true;
+                return false;
+            };
+            expr rhs_n = normalize(*m_tc[relax], rhs, is_target_fn, cs);
+            if (rhs != rhs_n && process_constraints(cs))
+                return process_metavar_eq(lhs, rhs_n, j, relax);
         }
         switch (status) {
         case occurs_check_status::FailLocal:

tests/lean/run/vector3.lean

@@ -0,0 +1,33 @@
+import logic data.nat.basic
+open nat
+
+inductive vector (A : Type) : nat → Type :=
+vnil  : vector A zero,
+vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+
+namespace vector
+  definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type :=
+  cases_on v₁
+    (cases_on v₂
+      (P → P)
+      (λ n₂ h₂ t₂, P))
+    (λ n₁ h₁ t₁, cases_on v₂
+      P
+      (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P))
+
+  definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ :=
+  assume H₁₂ : v₁ = v₂,
+    have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from
+      take H₁₁, cases_on v₁
+        (assume h : P, h)
+        (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P),
+          h rfl rfl rfl),
+    eq.rec aux H₁₂ H₁₂
+
+  theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
+  assume h, no_confusion h (λ n h t, h)
+
+  theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ :=
+  assume h, no_confusion h (λ n h t, t)
+
+end vector