fix(library/unifier): broken optimization in the unifier

See new comments and tests for details.

library/data/quotient/classical.lean

@@ -34,9 +34,12 @@ have H3 : ∀c, R a c ↔ R b c, from
     iff.intro
       (assume H4 : R a c, transR (symmR H2) H4)
       (assume H4 : R b c, transR H2 H4),
-have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)),
-show @epsilon _ (nonempty.intro a) (λc, R a c) = @epsilon _ (nonempty.intro b) (λc, R b c),
-  from congr_arg _ H4
+have H4 : (fun c, R a c) = (fun c, R b c), from
+  funext (take c, iff_to_eq (H3 c)),
+have H5 [visible] : nonempty A, from
+  nonempty.intro a,
+show epsilon (λc, R a c) = epsilon (λc, R b c), from
+  congr_arg _ H4
 
 definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R)
 

library/hott/equiv.lean

@@ -130,6 +130,8 @@ namespace IsEquiv
   variables {A B : Type} (f : A → B) (g : B → A)
             (retr : Sect g f) (sect : Sect f g)
 
+  context
+  set_option unifier.max_steps 30000
   --To construct an equivalence it suffices to state the proof that the inverse is a quasi-inverse.
   definition adjointify : IsEquiv f :=
     let sect' := (λx, ap g (ap f ((sect x)⁻¹))  ⬝  ap g (retr (f x))  ⬝  sect x) in
@@ -163,6 +165,7 @@ namespace IsEquiv
         from moveR_M1 _ _ eq3,
       eq4) in
     IsEquiv_mk g retr sect' adj'
+  end
 end IsEquiv
 
 namespace IsEquiv

library/hott/path.lean

@@ -8,7 +8,7 @@
 -- o Try doing these proofs with tactics.
 -- o Try using the simplifier on some of these proofs.
 
-import general_notation algebra.function
+import general_notation algebra.function tools.tactic
 
 open function
 
@@ -344,8 +344,11 @@ rec_on q idp
 definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
     {z : A} (s : g y ≈ z) :
   p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) :=
-rec_on s (rec_on q (concat_1p _ ▹ idp))
-
+begin
+  apply (rec_on s),
+  apply (rec_on q),
+  apply (concat_1p _ ▹ idp)
+end
 
 -- Action of [apD10] and [ap10] on paths
 -- -------------------------------------

src/library/unifier.cpp

@@ -1635,21 +1635,44 @@ struct unifier_fn {
 
         expr mk_imitiation_arg(expr const & arg, expr const & type, buffer<expr> const & locals,
                                constraint_seq & cs) {
-            if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) {
-                return arg;
+            // The following optimization is broken. It does not really work when we have dependent
+            // types. The problem is that the type of arg may depend on other arguments,
+            // and constraints are not generated to enforce it.
+            //
+            //  Here is a minimal counterexample
+            //     ?M A B a b H B b  =?=  heq.type_eq A B a b H
+            //  with this optimization the imitation is
+            //
+            //    ?M := fun (A B a b H B' b'), heq.type_eq A (?M1 A B a b H B' b') a (?M2 A B a b H B' b') H
+            //
+            //  This imitation is only correct if
+            //     typeof(H) is (heq A a (?M1 A B a b H B' b') (?M2 A B a b H B' b'))
+            //
+            //  Adding an extra constraint is problematic since typeof(H) may contain local constants,
+            //  and these local constants may have been "renamed" by mk_local_context above
+            //
+            //  For now, we simply comment the optimization.
+            //
+
+            // Broken optimization
+            // if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) {
+            //    return arg;
+            // }
+
+            // The following code is not affected by the problem above because we
+            // attach the type \c type to the new metavariables being created.
+
+            // std::cout << "type: " << type << "\n";
+            if (context_check(type, locals)) {
+                expr maux    = mk_metavar(u.m_ngen.next(), Pi(locals, type));
+                // std::cout << "  >> " << maux << " : " << mlocal_type(maux) << "\n";
+                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
+                return mk_app(maux, locals);
             } else {
-                // std::cout << "type: " << type << "\n";
-                if (context_check(type, locals)) {
-                    expr maux    = mk_metavar(u.m_ngen.next(), Pi(locals, type));
-                    // std::cout << "  >> " << maux << " : " << mlocal_type(maux) << "\n";
-                    cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
-                    return mk_app(maux, locals);
-                } else {
-                    expr maux_type   = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
-                    expr maux        = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
-                    cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
-                    return mk_app(maux, locals);
-                }
+                expr maux_type   = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
+                expr maux        = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
+                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
+                return mk_app(maux, locals);
             }
         }
 

tests/lean/slow/path_groupoids.lean

@@ -12,6 +12,7 @@ infixl `∘`:60 := compose
 
 -- Path
 -- ----
+set_option unifier.max_steps 100000
 
 inductive path {A : Type} (a : A) : A → Type :=
 idpath : path a a

tests/lean/unifier_bug.lean

@@ -0,0 +1,7 @@
+import logic
+
+theorem test {A B : Type} {a : A} {b : B} (H : a == b) :
+           eq.rec_on (heq.type_eq H) a = b
+:=
+-- Remark the error message should not occur in the token theorem
+heq.rec_on H rfl

tests/lean/unifier_bug.lean.expected.out

@@ -0,0 +1,8 @@
+unifier_bug.lean:7:0: error: type mismatch at application
+  heq.rec_on H rfl
+term
+  rfl
+has type
+  eq.rec_on (heq.type_eq H) a = eq.rec_on (heq.type_eq H) a
+but is expected to have type
+  eq.rec_on (heq.type_eq H) a = b