From 6a78ae7b46dbf1b7a2aa1c0b13e2e5cb620f67df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Mar 2015 10:27:05 -0700
Subject: [PATCH] fix(library/tactic/class_instance_synth): enforce consistent
 behavior in type class resolution

Auxiliary procedure mk_class_instance was not discarding partial solutions.
This procedure is used by the apply and inversion (aka cases) tactics
---
 src/library/tactic/class_instance_synth.cpp | 14 ++-
 tests/lean/hott/len_eq.hlean                | 96 +++++++++++++++++++++
 2 files changed, 106 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/hott/len_eq.hlean

diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index 4426df223..ea46c6389 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -466,10 +466,16 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
     new_cfg.m_pattern        = true;
     new_cfg.m_kind           = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal;
     try {
-        auto p  = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg).pull();
-        lean_assert(p);
-        substitution s = p->first.first;
-        return some_expr(s.instantiate_all(meta));
+        auto seq = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg);
+        while (true) {
+            auto p = seq.pull();
+            lean_assert(p);
+            substitution s = p->first.first;
+            expr r = s.instantiate_all(meta);
+            if (!has_expr_metavar_relaxed(r))
+                return some_expr(r);
+            seq = p->second;
+        }
     } catch (exception &) {
         return none_expr();
     }
diff --git a/tests/lean/hott/len_eq.hlean b/tests/lean/hott/len_eq.hlean
new file mode 100644
index 000000000..65c32ac31
--- /dev/null
+++ b/tests/lean/hott/len_eq.hlean
@@ -0,0 +1,96 @@
+import init.axioms.ua
+open nat unit equiv is_trunc
+
+inductive vector (A : Type) : nat → Type :=
+| nil {} : vector A zero
+| cons   : Π {n}, A → vector A n → vector A (succ n)
+
+open vector
+notation a :: b := cons a b
+
+definition const {A : Type} : Π (n : nat), A → vector A n
+| zero     a := nil
+| (succ n) a := a :: const n a
+
+definition head {A : Type} : Π {n : nat}, vector A (succ n) → A
+| n (x :: xs) := x
+
+theorem singlenton_vector_unit : ∀ {n : nat} (v w : vector unit n), v = w
+| zero     nil        nil        := rfl
+| (succ n) (star::xs) (star::ys) :=
+  begin
+    have h₁ : xs = ys, from singlenton_vector_unit xs ys,
+    rewrite h₁
+  end
+
+private definition f (n m : nat) (v : vector unit n) : vector unit m := const m star
+
+theorem vn_eqv_vm (n m : nat) : vector unit n ≃ vector unit m :=
+equiv.MK (f n m) (f m n)
+  (take v : vector unit m, singlenton_vector_unit (f n m (f m n v)) v)
+  (take v : vector unit n, singlenton_vector_unit (f m n (f n m v)) v)
+
+theorem vn_eq_vm (n m : nat) : vector unit n = vector unit m :=
+ua (vn_eqv_vm n m)
+
+definition vector_inj (A : Type) := ∀ (n m : nat), vector A n = vector A m → n = m
+
+theorem not_vector_inj : ¬ vector_inj unit :=
+assume H : vector_inj unit,
+have aux₁ : 0 = 1, from H 0 1 (vn_eq_vm 0 1),
+lift.down (nat.no_confusion aux₁)
+
+definition cast {A B : Type} (H : A = B) (a : A) : B :=
+eq.rec_on H a
+
+open sigma
+
+definition heq {A B : Type} (a : A) (b : B) :=
+Σ (H : A = B), cast H a = b
+
+infix `==`:50 := heq
+
+definition heq.type_eq {A B : Type} {a : A} {b : B} : a == b → A = B
+| ⟨H, e⟩ := H
+
+definition heq.symm : ∀ {A B : Type} {a : A} {b : B}, a == b → b == a
+| A A a a ⟨eq.refl A, eq.refl a⟩ :=  ⟨eq.refl A, eq.refl a⟩
+
+definition heq.trans : ∀ {A B C : Type} {a : A} {b : B} {c : C}, a == b → b == c → a == c
+| A A A a a a ⟨eq.refl A, eq.refl a⟩ ⟨eq.refl A, eq.refl a⟩ := ⟨eq.refl A, eq.refl a⟩
+
+theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
+| A A (eq.refl A) a := ⟨eq.refl A, eq.refl a⟩
+
+definition default (A : Type) [H : inhabited A] : A :=
+inhabited.rec_on H (λ a, a)
+
+definition lem_eq (A : Type) : Type :=
+∀ (n m : nat) (v : vector A n) (w : vector A m), v == w → n = m
+
+theorem lem_eq_iff_vector_inj (A : Type) [inh : inhabited A] : lem_eq A ↔ vector_inj A :=
+iff.intro
+  (assume Hl : lem_eq A,
+   assume n m he,
+   assert a : A, from default A,
+   assert v : vector A n, from const n a,
+   have e₁  : v == cast he v, from heq.symm (cast_heq he v),
+   Hl n m v (cast he v) e₁)
+  (assume Hr : vector_inj A,
+   assume n m v w he,
+   Hr n m (heq.type_eq he))
+
+theorem lem_eq_of_not_inhabited (A : Type) [ninh : inhabited A → empty] : lem_eq A :=
+take (n m : nat),
+match n with
+| zero      :=
+  match m with
+  | zero      := take v w He, rfl
+  | (succ m₁) :=
+    take (v : vector A zero) (w : vector A (succ m₁)),
+    empty.elim _ (ninh (inhabited.mk (head w)))
+  end
+| (succ n₁) :=
+  take (v : vector A (succ n₁)) (w : vector A m),
+  empty.elim _ (ninh (inhabited.mk (head v)))
+end