fix(library/unifier): postpone class-instance constraints whose type could not be inferred

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

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)) {

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

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 _)