From 8295ef4e573488581a6d379b8d7f3c17acc82b23 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Mar 2015 22:20:20 -0800 Subject: [PATCH] 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 | 2 ++ hott/init/equiv.hlean | 1 + src/library/tactic/class_instance_synth.cpp | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index cf2a7aee4..164aaba98 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/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 diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index df0f4b52b..cdba8f499 100644 --- a/hott/init/equiv.hlean +++ b/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) := diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index 3c17c1b90..5ba8d7fc4 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -316,7 +316,7 @@ constraint mk_class_instance_cnstr(std::shared_ptr 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); }