From 06f436840fa17ac53efe263709de523c0dd81629 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Dec 2014 22:27:23 -0800
Subject: [PATCH] fix(library/unifier): postpone class-instance constraints
 whose type could not be inferred

---
 library/hott/types/sigma.lean          |  4 +++-
 src/library/unifier.cpp                | 16 ++++++++++++++--
 tests/lean/run/apply_class_issue.lean  | 18 ++++++++++++++++++
 tests/lean/run/apply_class_issue0.lean |  6 ++++++
 4 files changed, 41 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/apply_class_issue.lean
 create mode 100644 tests/lean/run/apply_class_issue0.lean

diff --git a/library/hott/types/sigma.lean b/library/hott/types/sigma.lean
index b0b02f8f3..756885137 100644
--- a/library/hott/types/sigma.lean
+++ b/library/hott/types/sigma.lean
@@ -349,7 +349,9 @@ begin
          apply equiv_path_sigma,
          apply IH,
            apply succ_is_trunc,
-           intro aa, apply (succ_is_trunc (aa ▹ u.2) (v.2)),
+           intro aa,
+             show is_trunc n (aa ▹ u .2 ≈ v .2), from
+             succ_is_trunc (aa ▹ u.2) (v.2),
 end
 
 end sigma
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 526dc47ea..67c296d91 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1960,9 +1960,13 @@ struct unifier_fn {
             return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
     }
 
+    void postpone(constraint const & c) {
+        m_postponed = cons(c, m_postponed);
+    }
+
     void discard(constraint const & c) {
         if (!m_config.m_discard)
-            m_postponed = cons(c, m_postponed);
+            postpone(c);
     }
 
     bool process_flex_flex(constraint const & c) {
@@ -2184,10 +2188,18 @@ struct unifier_fn {
     bool process_next() {
         lean_assert(!m_cnstrs.empty());
         auto const * p = m_cnstrs.min();
+        constraint c   = p->first;
         unsigned cidx  = p->second;
+        if (cidx >= get_group_first_index(cnstr_group::ClassInstance) &&
+            !m_config.m_discard && cnstr_on_demand(c)) {
+            // we postpone class-instance constraints whose type still contains metavariables
+            m_cnstrs.erase_min();
+            postpone(c);
+            return true;
+        }
+        // The following condition is "dead-code"
         if (!m_config.m_expensive_classes && cidx >= get_group_first_index(cnstr_group::ClassInstance))
             m_pattern = true; // use only higher-order (pattern) matching after we start processing class-instance constraints
-        constraint c   = p->first;
         // std::cout << "process_next: " << c << "\n";
         m_cnstrs.erase_min();
         if (is_choice_cnstr(c)) {
diff --git a/tests/lean/run/apply_class_issue.lean b/tests/lean/run/apply_class_issue.lean
new file mode 100644
index 000000000..d0035b74c
--- /dev/null
+++ b/tests/lean/run/apply_class_issue.lean
@@ -0,0 +1,18 @@
+import hott.trunc
+open truncation
+--structure is_contr [class] (A : Type) : Type
+
+context
+parameters {P : Π(A : Type), A → Prop}
+
+definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
+
+definition foo2
+(A : Type)
+(B : A → Type)
+(a : A)
+(x : B a)
+(H : Π (a : A), is_contr (B a))  --(H : is_contr (B a))
+  : P (B a) x :=
+by apply (@my_contr _ _)
+end
diff --git a/tests/lean/run/apply_class_issue0.lean b/tests/lean/run/apply_class_issue0.lean
new file mode 100644
index 000000000..48cb99c4b
--- /dev/null
+++ b/tests/lean/run/apply_class_issue0.lean
@@ -0,0 +1,6 @@
+structure is_trunc [class] (A : Type) : Type
+
+theorem foo (A : Type) [H : is_trunc A] (B : Type) : B := sorry
+
+theorem bar [H : is_trunc false] : false :=
+by apply (@foo false _)