Consistent and higher precedence for default [Equiv] instances on maps/collections.

theories/collections.v

@@ -7,11 +7,13 @@ From stdpp Require Export orders list.
 (* FIXME: This file needs a 'Proof Using' hint, but the default we use
    everywhere makes for lots of extra ssumptions. *)
 
-Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
+(* Higher precedence to make sure these instances are not used for other types
+with an [ElemOf] instance, such as lists. *)
+Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
-Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
+Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
+Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
 Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
 

theories/fin_maps.v

@@ -80,7 +80,9 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
 Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
   λ f, merge (difference_with f).
 
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+(** Higher precedence to make sure it's not used for other types with a [Lookup]
+instance, such as lists. *)
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the