fix(library/tactic/class_instance_synth): constraint execution order at type class resolution

We could not fix this problem before because we did not have the
[quasireducible] annotation.

Without this annotation, the fixed TC would loop in some HoTT files.

hott/algebra/precategory/iso.hlean

@@ -22,6 +22,8 @@ namespace iso
     (left_inverse  : inverse ∘ f = id)
     (right_inverse : f ∘ inverse = id)
 
+  attribute is_iso.inverse [quasireducible]
+
   attribute is_iso [multiple-instances]
   open split_mono split_epi is_iso
   definition retraction_of [reducible] := @split_mono.retraction_of

hott/init/equiv.hlean

@@ -22,6 +22,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) :=
   (sect : (inv ∘ f) ∼ id)
   (adj : Πx, retr (f x) = ap f (sect x))
 
+attribute is_equiv.inv [quasireducible]
 
 -- A more bundled version of equivalence
 structure equiv (A B : Type) :=

src/library/tactic/class_instance_synth.cpp

@@ -316,7 +316,7 @@ constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const
     };
     bool owner      = false;
     bool relax      = C->m_relax;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance),
+    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic),
                            owner, j, relax);
 }