From 7d7c9871312719a4e1296d52eb95ea0ac959249f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Sep 2017 10:57:05 +0200
Subject: [PATCH] Set Hint Mode for all classes in `base.v`.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None ↔ m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None ↔ m !! j = None.

That is, we have to specify the type of `m`.
---
 theories/base.v            |  43 +++++++++-
 theories/coPset.v          |   2 +-
 theories/collections.v     | 108 ++++++++++++------------
 theories/fin_collections.v |  10 +--
 theories/fin_map_dom.v     |  11 +--
 theories/fin_maps.v        | 163 ++++++++++++++++++++-----------------
 theories/gmap.v            |   8 +-
 theories/gmultiset.v       |  39 ++-------
 theories/hashset.v         |  37 +++------
 theories/list.v            |  31 +++----
 theories/listset.v         |  40 +++------
 theories/mapset.v          |  41 +++-------
 theories/option.v          |   8 +-
 theories/set.v             |   4 +-
 14 files changed, 273 insertions(+), 272 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 323dd30d..fb129db3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -94,6 +94,9 @@ Proof. split; repeat intro; congruence. Qed.
 (** We define an operational type class for setoid equality. This is based on
 (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
+(* No Hint Mode set because of Coq bug #5735
+Hint Mode Equiv ! : typeclass_instances. *)
+
 Infix "≡" := equiv (at level 70, no associativity) : C_scope.
 Notation "(≡)" := equiv (only parsing) : C_scope.
 Notation "( X ≡)" := (equiv X) (only parsing) : C_scope.
@@ -108,10 +111,12 @@ with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
 reverse. *)
 Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
+Hint Mode LeibnizEquiv ! - : typeclass_instances.
+
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
   x ≡ y ↔ x = y.
 Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
- 
+
 Ltac fold_leibniz := repeat
   match goal with
   | H : context [ @equiv ?A _ _ _ ] |- _ =>
@@ -149,12 +154,14 @@ propositions. For example to declare a parameter expressing decidable equality
 on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
 [decide (x = y)]. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
+Hint Mode Decision ! : typeclass_instances.
 Arguments decide _ {_} : assert.
 Notation EqDecision A := (∀ x y : A, Decision (x = y)).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
 Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
+Hint Mode Inhabited ! : typeclass_instances.
 Arguments populate {_} _ : assert.
 
 (** ** Proof irrelevant types *)
@@ -162,6 +169,7 @@ Arguments populate {_} _ : assert.
 elements of the type are equal. We use this notion only used for propositions,
 but by universe polymorphism we can generalize it. *)
 Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
+Hint Mode ProofIrrel ! : typeclass_instances.
 
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
@@ -625,14 +633,17 @@ relations on collections: the empty collection [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
 Class Empty A := empty: A.
+Hint Mode Empty ! : typeclass_instances.
 Notation "∅" := empty : C_scope.
 
 Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Top A := top : A.
+Hint Mode Top ! : typeclass_instances.
 Notation "⊤" := top : C_scope.
 
 Class Union A := union: A → A → A.
+Hint Mode Union ! : typeclass_instances.
 Instance: Params (@union) 2.
 Infix "∪" := union (at level 50, left associativity) : C_scope.
 Notation "(∪)" := union (only parsing) : C_scope.
@@ -650,6 +661,7 @@ Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.
 
 Class Intersection A := intersection: A → A → A.
+Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2.
 Infix "∩" := intersection (at level 40) : C_scope.
 Notation "(∩)" := intersection (only parsing) : C_scope.
@@ -657,6 +669,7 @@ Notation "( x ∩)" := (intersection x) (only parsing) : C_scope.
 Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A → A → A.
+Hint Mode Difference ! : typeclass_instances.
 Instance: Params (@difference) 2.
 Infix "∖" := difference (at level 40, left associativity) : C_scope.
 Notation "(∖)" := difference (only parsing) : C_scope.
@@ -670,6 +683,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
   (at level 50, left associativity) : C_scope.
 
 Class Singleton A B := singleton: A → B.
+Hint Mode Singleton - ! : typeclass_instances.
 Instance: Params (@singleton) 3.
 Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
@@ -681,6 +695,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z))
   (at level 1, y at next level, z at next level) : C_scope.
 
 Class SubsetEq A := subseteq: relation A.
+Hint Mode SubsetEq ! : typeclass_instances.
 Instance: Params (@subseteq) 2.
 Infix "⊆" := subseteq (at level 70) : C_scope.
 Notation "(⊆)" := subseteq (only parsing) : C_scope.
@@ -720,8 +735,10 @@ Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level)
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
 Class Lexico A := lexico: relation A.
+Hint Mode Lexico ! : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
+Hint Mode ElemOf - ! : typeclass_instances.
 Instance: Params (@elem_of) 3.
 Infix "∈" := elem_of (at level 70) : C_scope.
 Notation "(∈)" := elem_of (only parsing) : C_scope.
@@ -733,6 +750,7 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
 Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
+Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2.
 Infix "⊥" := disjoint (at level 70) : C_scope.
 Notation "(⊥)" := disjoint (only parsing) : C_scope.
@@ -749,6 +767,7 @@ Hint Extern 0 (_ ⊥ _) => symmetry; eassumption.
 Hint Extern 0 (_ ⊥* _) => symmetry; eassumption.
 
 Class DisjointE E A := disjointE : E → A → A → Prop.
+Hint Mode DisjointE - ! : typeclass_instances.
 Instance: Params (@disjointE) 4.
 Notation "X ⊥{ Γ } Y" := (disjointE Γ X Y)
   (at level 70, format "X  ⊥{ Γ }  Y") : C_scope.
@@ -765,11 +784,14 @@ Notation "Xs ⊥{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
 Hint Extern 0 (_ ⊥{_} _) => symmetry; eassumption.
 
 Class DisjointList A := disjoint_list : list A → Prop.
+Hint Mode DisjointList ! : typeclass_instances.
 Instance: Params (@disjoint_list) 2.
 Notation "⊥ Xs" := (disjoint_list Xs) (at level 20, format "⊥  Xs") : C_scope.
 
 Section disjoint_list.
   Context `{Disjoint A, Union A, Empty A}.
+  Implicit Types X : A.
+
   Inductive disjoint_list_default : DisjointList A :=
     | disjoint_nil_2 : ⊥ (@nil A)
     | disjoint_cons_2 (X : A) (Xs : list A) : X ⊥ ⋃ Xs → ⊥ Xs → ⊥ (X :: Xs).
@@ -782,8 +804,10 @@ Section disjoint_list.
 End disjoint_list.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
+Hint Mode Filter - ! : typeclass_instances.
 
 Class UpClose A B := up_close : A → B.
+Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
@@ -850,6 +874,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
+Hint Mode Lookup - - ! : typeclass_instances.
 Instance: Params (@lookup) 4.
 Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
 Notation "(!!)" := lookup (only parsing) : C_scope.
@@ -859,12 +884,14 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
+Hint Mode SingletonM - - ! : typeclass_instances.
 Instance: Params (@singletonM) 5.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
+Hint Mode Insert - - ! : typeclass_instances.
 Instance: Params (@insert) 5.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
@@ -874,12 +901,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
+Hint Mode Delete - ! : typeclass_instances.
 Instance: Params (@delete) 4.
 Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
+Hint Mode Alter - - ! : typeclass_instances.
 Instance: Params (@alter) 5.
 Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -889,12 +918,14 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
+Hint Mode PartialAlter - - ! : typeclass_instances.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
+Hint Mode Dom ! ! : typeclass_instances.
 Instance: Params (@dom) 3.
 Arguments dom : clear implicits.
 Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
@@ -903,6 +934,7 @@ Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
+Hint Mode Merge ! : typeclass_instances.
 Instance: Params (@merge) 4.
 Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -911,17 +943,20 @@ and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
+Hint Mode UnionWith - ! : typeclass_instances.
 Instance: Params (@union_with) 3.
 Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
+Hint Mode IntersectionWith - ! : typeclass_instances.
 Instance: Params (@intersection_with) 3.
 Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
+Hint Mode DifferenceWith - ! : typeclass_instances.
 Instance: Params (@difference_with) 3.
 Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -930,6 +965,7 @@ Definition intersection_with_list `{IntersectionWith A M}
 Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 
 Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
+Hint Mode LookupE - - - ! : typeclass_instances.
 Instance: Params (@lookupE) 6.
 Notation "m !!{ Γ } i" := (lookupE Γ i m)
   (at level 20, format "m  !!{ Γ }  i") : C_scope.
@@ -937,6 +973,7 @@ Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
 Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
+Hint Mode InsertE - - - ! : typeclass_instances.
 Instance: Params (@insertE) 6.
 Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
   (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
@@ -963,6 +1000,7 @@ Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
+Hint Mode Elements - ! : typeclass_instances.
 Instance: Params (@elements) 3.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
@@ -998,6 +1036,7 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   NoDup_elements X : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
+Hint Mode Size ! : typeclass_instances.
 Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2.
 
@@ -1025,6 +1064,7 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A),
 will later prove that [fresh] is [Proper] with respect to the induced setoid
 equality on collections. *)
 Class Fresh A C := fresh: C → A.
+Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3.
 Class FreshSpec A C `{ElemOf A C,
     Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
@@ -1035,5 +1075,6 @@ Class FreshSpec A C `{ElemOf A C,
 
 (** * Miscellaneous *)
 Class Half A := half: A → A.
+Hint Mode Half ! : typeclass_instances.
 Notation "½" := half : C_scope.
 Notation "½*" := (fmap (M:=list) half) : C_scope.
diff --git a/theories/coPset.v b/theories/coPset.v
index 68b8466f..4af9f023 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -427,7 +427,7 @@ Proof.
   rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
   induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
 Qed.
-Lemma coPset_split X :
+Lemma coPset_split (X : coPset) :
   ¬set_finite X →
   ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ ¬set_finite X1 ∧ ¬set_finite X2.
 Proof.
diff --git a/theories/collections.v b/theories/collections.v
index bb6c4b5f..134af648 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -145,9 +145,9 @@ Section set_unfold_simple.
   Implicit Types x y : A.
   Implicit Types X Y : C.
 
-  Global Instance set_unfold_empty x : SetUnfold (x ∈ ∅) False.
+  Global Instance set_unfold_empty x : SetUnfold (x ∈ (∅ : C)) False.
   Proof. constructor. split. apply not_elem_of_empty. done. Qed.
-  Global Instance set_unfold_singleton x y : SetUnfold (x ∈ {[ y ]}) (x = y).
+  Global Instance set_unfold_singleton x y : SetUnfold (x ∈ ({[ y ]} : C)) (x = y).
   Proof. constructor; apply elem_of_singleton. Qed.
   Global Instance set_unfold_union x X Y P Q :
     SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∪ Y) (P ∨ Q).
@@ -161,30 +161,30 @@ Section set_unfold_simple.
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
   Proof.
     intros ?; constructor. unfold equiv, collection_equiv.
-    pose proof not_elem_of_empty; naive_solver.
+    pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
-  Global Instance set_unfold_equiv_empty_r (P : A → Prop) :
+  Global Instance set_unfold_equiv_empty_r (P : A → Prop) X :
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
   Proof.
     intros ?; constructor. unfold equiv, collection_equiv.
-    pose proof not_elem_of_empty; naive_solver.
+    pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
-  Global Instance set_unfold_equiv (P Q : A → Prop) :
+  Global Instance set_unfold_equiv (P Q : A → Prop) X :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X ≡ Y) (∀ x, P x ↔ Q x) | 10.
   Proof. constructor. apply forall_proper; naive_solver. Qed.
-  Global Instance set_unfold_subseteq (P Q : A → Prop) :
+  Global Instance set_unfold_subseteq (P Q : A → Prop) X Y :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X ⊆ Y) (∀ x, P x → Q x).
   Proof. constructor. apply forall_proper; naive_solver. Qed.
-  Global Instance set_unfold_subset (P Q : A → Prop) :
+  Global Instance set_unfold_subset (P Q : A → Prop) X :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X ⊂ Y) ((∀ x, P x → Q x) ∧ ¬∀ x, Q x → P x).
   Proof.
     constructor. unfold strict.
     repeat f_equiv; apply forall_proper; naive_solver.
   Qed.
-  Global Instance set_unfold_disjoint (P Q : A → Prop) :
+  Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X ⊥ Y) (∀ x, P x → Q x → False).
   Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
@@ -195,10 +195,10 @@ Section set_unfold_simple.
   Global Instance set_unfold_equiv_empty_l_L X (P : A → Prop) :
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ = X) (∀ x, ¬P x) | 5.
   Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed.
-  Global Instance set_unfold_equiv_empty_r_L (P : A → Prop) :
+  Global Instance set_unfold_equiv_empty_r_L (P : A → Prop) X :
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X = ∅) (∀ x, ¬P x) | 5.
   Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed.
-  Global Instance set_unfold_equiv_L (P Q : A → Prop) :
+  Global Instance set_unfold_equiv_L (P Q : A → Prop) X Y :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X = Y) (∀ x, P x ↔ Q x) | 10.
   Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed.
@@ -224,20 +224,20 @@ Section set_unfold.
 End set_unfold.
 
 Section set_unfold_monad.
-  Context `{CollectionMonad M} {A : Type}.
-  Implicit Types x y : A.
+  Context `{CollectionMonad M}.
 
-  Global Instance set_unfold_ret x y : SetUnfold (x ∈ mret y) (x = y).
+  Global Instance set_unfold_ret {A} (x y : A) :
+    SetUnfold (x ∈ mret (M:=M) y) (x = y).
   Proof. constructor; apply elem_of_ret. Qed.
-  Global Instance set_unfold_bind {B} (f : A → M B) X (P Q : A → Prop) :
+  Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) :
     (∀ y, SetUnfold (y ∈ X) (P y)) → (∀ y, SetUnfold (x ∈ f y) (Q y)) →
     SetUnfold (x ∈ X ≫= f) (∃ y, Q y ∧ P y).
   Proof. constructor. rewrite elem_of_bind; naive_solver. Qed.
-  Global Instance set_unfold_fmap {B} (f : A → B) X (P : A → Prop) :
+  Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) :
     (∀ y, SetUnfold (y ∈ X) (P y)) →
     SetUnfold (x ∈ f <$> X) (∃ y, x = f y ∧ P y).
   Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed.
-  Global Instance set_unfold_join (X : M (M A)) (P : M A → Prop) :
+  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) :
     (∀ Y, SetUnfold (Y ∈ X) (P Y)) → SetUnfold (x ∈ mjoin X) (∃ Y, x ∈ Y ∧ P Y).
   Proof. constructor. rewrite elem_of_join; naive_solver. Qed.
 End set_unfold_monad.
@@ -381,7 +381,7 @@ Section simple_collection.
   Proof. set_solver. Qed.
   Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X.
   Proof. set_solver. Qed.
-  Lemma elem_of_empty x : x ∈ ∅ ↔ False.
+  Lemma elem_of_empty x : x ∈ (∅ : C) ↔ False.
   Proof. set_solver. Qed.
   Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅.
   Proof. set_solver. Qed.
@@ -393,15 +393,15 @@ Section simple_collection.
   Proof. set_solver. Qed.
 
   (** Singleton *)
-  Lemma elem_of_singleton_1 x y : x ∈ {[y]} → x = y.
+  Lemma elem_of_singleton_1 x y : x ∈ ({[y]} : C) → x = y.
   Proof. by rewrite elem_of_singleton. Qed.
-  Lemma elem_of_singleton_2 x y : x = y → x ∈ {[y]}.
+  Lemma elem_of_singleton_2 x y : x = y → x ∈ ({[y]} : C).
   Proof. by rewrite elem_of_singleton. Qed.
   Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
   Proof. set_solver. Qed.
   Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅.
   Proof. set_solver. Qed.
-  Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
+  Lemma not_elem_of_singleton x y : x ∉ ({[ y ]} : C) ↔ x ≠ y.
   Proof. by rewrite elem_of_singleton. Qed.
 
   (** Disjointness *)
@@ -512,7 +512,7 @@ Section simple_collection.
     Proof. unfold_leibniz. apply non_empty_inhabited. Qed.
 
     (** Singleton *)
-    Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅.
+    Lemma non_empty_singleton_L x : {[ x ]} ≠ (∅ : C).
     Proof. unfold_leibniz. apply non_empty_singleton. Qed.
 
     (** Big unions *)
@@ -554,6 +554,7 @@ End simple_collection.
 (** * Collections with [∪], [∩], [∖], [∅] and [{[_]}] *)
 Section collection.
   Context `{Collection A C}.
+  Implicit Types x y : A.
   Implicit Types X Y : C.
 
   (** Intersection *)
@@ -654,7 +655,7 @@ Section collection.
     Global Instance intersection_empty_r_L: RightAbsorb ((=) : relation C) ∅ (∩).
     Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
 
-    Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = {[x]}.
+    Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = ({[x]} : C).
     Proof. unfold_leibniz. apply intersection_singletons. Qed.
 
     Lemma union_intersection_l_L X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
@@ -719,7 +720,7 @@ Section collection.
       {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
     Proof.
       intro y; split; intros Hy; [ set_solver | ].
-      destruct (decide (y ∈ {[x]})); set_solver.
+      destruct (decide (y ∈ ({[x]} : C))); set_solver.
     Qed.
 
     Context `{!LeibnizEquiv C}.
@@ -736,7 +737,6 @@ Section collection.
     Lemma singleton_union_difference_L X Y x :
       {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
     Proof. unfold_leibniz. apply singleton_union_difference. Qed.
-
   End dec.
 End collection.
 
@@ -751,26 +751,26 @@ Section of_option_list.
   Context `{SimpleCollection A C}.
   Implicit Types l : list A.
 
-  Lemma elem_of_of_option (x : A) mx: x ∈ of_option mx ↔ mx = Some x.
+  Lemma elem_of_of_option (x : A) mx: x ∈ of_option (C:=C) mx ↔ mx = Some x.
   Proof. destruct mx; set_solver. Qed.
-  Lemma not_elem_of_of_option (x : A) mx: x ∉ of_option mx ↔ mx ≠ Some x.
+  Lemma not_elem_of_of_option (x : A) mx: x ∉ of_option (C:=C) mx ↔ mx ≠ Some x.
   Proof. by rewrite elem_of_of_option. Qed.
 
-  Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l.
+  Lemma elem_of_of_list (x : A) l : x ∈ of_list (C:=C) l ↔ x ∈ l.
   Proof.
     split.
     - induction l; simpl; [by rewrite elem_of_empty|].
       rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
     - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
   Qed.
-  Lemma not_elem_of_of_list (x : A) l : x ∉ of_list l ↔ x ∉ l.
+  Lemma not_elem_of_of_list (x : A) l : x ∉ of_list (C:=C) l ↔ x ∉ l.
   Proof. by rewrite elem_of_of_list. Qed.
 
   Global Instance set_unfold_of_option (mx : option A) x :
-    SetUnfold (x ∈ of_option mx) (mx = Some x).
+    SetUnfold (x ∈ of_option (C:=C) mx) (mx = Some x).
   Proof. constructor; apply elem_of_of_option. Qed.
   Global Instance set_unfold_of_list (l : list A) x P :
-    SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list l) P.
+    SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list (C:=C) l) P.
   Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x ∈ l) P). Qed.
 
   Lemma of_list_nil : of_list (C:=C) [] = ∅.
@@ -810,7 +810,7 @@ Section collection_monad_base.
     rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
     destruct (decide P); naive_solver.
   Qed.
-  Global Instance set_unfold_guard `{Decision P} {A} (x : A) X Q :
+  Global Instance set_unfold_guard `{Decision P} {A} (x : A) (X : M A) Q :
     SetUnfold (x ∈ X) Q → SetUnfold (x ∈ guard P; X) (P ∧ Q).
   Proof. constructor. by rewrite elem_of_guard, (set_unfold (x ∈ X) Q). Qed.
   Lemma bind_empty {A B} (f : A → M B) X :
@@ -824,11 +824,12 @@ Definition set_Forall `{ElemOf A C} (P : A → Prop) (X : C) := ∀ x, x ∈ X 
 Definition set_Exists `{ElemOf A C} (P : A → Prop) (X : C) := ∃ x, x ∈ X ∧ P x.
 
 Section quantifiers.
-  Context `{SimpleCollection A B} (P : A → Prop).
+  Context `{SimpleCollection A C} (P : A → Prop).
+  Implicit Types X Y : C.
 
-  Lemma set_Forall_empty : set_Forall P ∅.
+  Lemma set_Forall_empty : set_Forall P (∅ : C).
   Proof. unfold set_Forall. set_solver. Qed.
-  Lemma set_Forall_singleton x : set_Forall P {[ x ]} ↔ P x.
+  Lemma set_Forall_singleton x : set_Forall P ({[ x ]} : C) ↔ P x.
   Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_union X Y :
     set_Forall P X → set_Forall P Y → set_Forall P (X ∪ Y).
@@ -838,9 +839,9 @@ Section quantifiers.
   Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y.
   Proof. unfold set_Forall. set_solver. Qed.
 
-  Lemma set_Exists_empty : ¬set_Exists P ∅.
+  Lemma set_Exists_empty : ¬set_Exists P (∅ : C).
   Proof. unfold set_Exists. set_solver. Qed.
-  Lemma set_Exists_singleton x : set_Exists P {[ x ]} ↔ P x.
+  Lemma set_Exists_singleton x : set_Exists P ({[ x ]} : C) ↔ P x.
   Proof. unfold set_Exists. set_solver. Qed.
   Lemma set_Exists_union_1 X Y : set_Exists P X → set_Exists P (X ∪ Y).
   Proof. unfold set_Exists. set_solver. Qed.
@@ -852,7 +853,8 @@ Section quantifiers.
 End quantifiers.
 
 Section more_quantifiers.
-  Context `{SimpleCollection A B}.
+  Context `{SimpleCollection A C}.
+  Implicit Types X : C.
 
   Lemma set_Forall_impl (P Q : A → Prop) X :
     set_Forall P X → (∀ x, P x → Q x) → set_Forall Q X.
@@ -987,15 +989,17 @@ End collection_monad.
 Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X → x ∈ l.
 
 Section finite.
-  Context `{SimpleCollection A B}.
+  Context `{SimpleCollection A C}.
+  Implicit Types X Y : C.
+
   Global Instance set_finite_subseteq :
-     Proper (flip (⊆) ==> impl) (@set_finite A B _).
+    Proper (flip (⊆) ==> impl) (@set_finite A C _).
   Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed.
-  Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A B _).
+  Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A C _).
   Proof. intros X Y HX; apply exist_proper. by setoid_rewrite HX. Qed.
-  Lemma empty_finite : set_finite ∅.
+  Lemma empty_finite : set_finite (∅ : C).
   Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
-  Lemma singleton_finite (x : A) : set_finite {[ x ]}.
+  Lemma singleton_finite (x : A) : set_finite ({[ x ]} : C).
   Proof. exists [x]; intros y ->%elem_of_singleton; left. Qed.
   Lemma union_finite X Y : set_finite X → set_finite Y → set_finite (X ∪ Y).
   Proof.
@@ -1009,7 +1013,9 @@ Section finite.
 End finite.
 
 Section more_finite.
-  Context `{Collection A B}.
+  Context `{Collection A C}.
+  Implicit Types X Y : C.
+
   Lemma intersection_finite_l X Y : set_finite X → set_finite (X ∩ Y).
   Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
   Lemma intersection_finite_r X Y : set_finite Y → set_finite (X ∩ Y).
@@ -1038,14 +1044,15 @@ Section seq_set.
   Implicit Types start len x : nat.
 
   Lemma elem_of_seq_set start len x :
-    x ∈ seq_set start len ↔ start ≤ x < start + len.
+    x ∈ seq_set (C:=C) start len ↔ start ≤ x < start + len.
   Proof.
     revert start. induction len as [|len IH]; intros start; simpl.
     - rewrite elem_of_empty. omega.
     - rewrite elem_of_union, elem_of_singleton, IH. omega.
   Qed.
 
-  Lemma seq_set_S_disjoint start len : {[ start + len ]} ⊥ seq_set start len.
+  Lemma seq_set_S_disjoint start len :
+    {[ start + len ]} ⊥ seq_set (C:=C) start len.
   Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
 
   Lemma seq_set_S_union start len :
@@ -1055,7 +1062,7 @@ Section seq_set.
   Qed.
 
   Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
-    seq_set start (S len) = {[ start + len ]} ∪ seq_set start len.
+    seq_set start (C:=C) (S len) = {[ start + len ]} ∪ seq_set start len.
   Proof. unfold_leibniz. apply seq_set_S_union. Qed.
 End seq_set.
 
@@ -1067,6 +1074,7 @@ Typeclasses Opaque minimal.
 
 Section minimal.
   Context `{SimpleCollection A C} {R : relation A}.
+  Implicit Types X Y : C.
 
   Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x).
   Proof. intros X X' y; unfold minimal; set_solver. Qed.
@@ -1085,11 +1093,11 @@ Section minimal.
     minimal R x X ↔ ∀ y, y ∈ X → ¬R y x.
   Proof. unfold minimal; split; [eauto using minimal_strict_1|naive_solver]. Qed.
 
-  Lemma empty_minimal x : minimal R x ∅.
+  Lemma empty_minimal x : minimal R x (∅ : C).
   Proof. unfold minimal; set_solver. Qed.
-  Lemma singleton_minimal x : minimal R x {[ x ]}.
+  Lemma singleton_minimal x : minimal R x ({[ x ]} : C).
   Proof. unfold minimal; set_solver. Qed.
-  Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x {[ y ]}.
+  Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x ({[ y ]} : C).
   Proof. unfold minimal; set_solver. Qed.
   Lemma union_minimal X Y x :
     minimal R x X → minimal R x Y → minimal R x (X ∪ Y).
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index f5061160..ddb1220c 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -63,14 +63,14 @@ Proof.
   intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
   by rewrite elem_of_cons, elem_of_elements.
 Qed.
-Lemma elements_singleton x : elements {[ x ]} = [x].
+Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
 Proof.
   apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
     elements_union_singleton, elements_empty by set_solver.
 Qed.
 Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
 Proof.
-  intros; apply NoDup_submseteq; auto using NoDup_elements.
+  intros; apply NoDup_submseteq; eauto using NoDup_elements.
   intros x. rewrite !elem_of_elements; auto.
 Qed.
 
@@ -106,7 +106,7 @@ Proof.
   contradict Hsz. rewrite HX, size_empty; lia.
 Qed.
 
-Lemma size_singleton (x : A) : size {[ x ]} = 1.
+Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
 Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
@@ -200,9 +200,9 @@ Proof.
   { destruct IH as (x' & Hx' & Hmin); [set_solver|].
     destruct (decide (R x x')).
     - exists x; split; [set_solver|].
-      eauto using union_minimal, singleton_minimal, minimal_weaken.
+      eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken.
     - exists x'; split; [set_solver|].
-      auto using union_minimal, singleton_minimal_not_above. }
+      eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). }
   exists x; split; [set_solver|].
   rewrite HX, (right_id _ (∪)). apply singleton_minimal.
 Qed.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 5be84036..68632ad6 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -61,7 +61,7 @@ Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
 Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} ≡ {[ i ]}.
+Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A) ≡ {[ i ]}.
 Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
@@ -100,7 +100,7 @@ Proof.
   unfold is_Some. setoid_rewrite lookup_difference_Some.
   destruct (m2 !! i); naive_solver.
 Qed.
-Lemma dom_fmap {A B} (f : A → B) m : dom D (f <$> m) ≡ dom D m.
+Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom D (f <$> m) ≡ dom D m.
 Proof.
   apply elem_of_equiv. intros i.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
@@ -109,7 +109,8 @@ Qed.
 Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
 Proof.
   induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
-    eauto using empty_finite, union_finite, singleton_finite.
+    eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
+    (singleton_finite (C:=D)).
 Qed.
 
 Context `{!LeibnizEquiv D}.
@@ -121,7 +122,7 @@ Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
 Proof. unfold_leibniz; apply dom_alter. Qed.
 Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
 Proof. unfold_leibniz; apply dom_insert. Qed.
-Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i := x]} = {[ i ]}.
+Lemma dom_singleton_L {A} (i : K) (x : A) : dom D ({[i := x]} : M A) = {[ i ]}.
 Proof. unfold_leibniz; apply dom_singleton. Qed.
 Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
 Proof. unfold_leibniz; apply dom_delete. Qed.
@@ -132,6 +133,6 @@ Lemma dom_intersection_L {A} (m1 m2 : M A) :
 Proof. unfold_leibniz; apply dom_intersection. Qed.
 Lemma dom_difference_L {A} (m1 m2 : M A) : dom D (m1 ∖ m2) = dom D m1 ∖ dom D m2.
 Proof. unfold_leibniz; apply dom_difference. Qed.
-Lemma dom_fmap_L {A B} (f : A → B) m : dom D (f <$> m) = dom D m.
+Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
 Proof. unfold_leibniz; apply dom_fmap. Qed.
 End fin_map_dom.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e9607aef..fcaba6ce 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -26,6 +26,8 @@ which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
 
 Class FinMapToList K A M := map_to_list: M → list (K * A).
+Hint Mode FinMapToList ! - - : typeclass_instances.
+Hint Mode FinMapToList - - ! : typeclass_instances.
 
 Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
@@ -213,7 +215,7 @@ Proof.
     specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 Global Instance map_included_preorder {A} (R : relation A) :
-  PreOrder R → PreOrder (map_included R).
+  PreOrder R → PreOrder (map_included R : relation (M A)).
 Proof.
   split; [intros m i; by destruct (m !! i); simpl|].
   intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
@@ -247,7 +249,7 @@ Lemma map_empty {A} (m : M A) : (∀ i, m !! i = None) → m = ∅.
 Proof. intros Hm. apply map_eq. intros. by rewrite Hm, lookup_empty. Qed.
 Lemma lookup_empty_is_Some {A} i : ¬is_Some ((∅ : M A) !! i).
 Proof. rewrite lookup_empty. by inversion 1. Qed.
-Lemma lookup_empty_Some {A} i (x : A) : ¬∅ !! i = Some x.
+Lemma lookup_empty_Some {A} i (x : A) : ¬(∅ : M A) !! i = Some x.
 Proof. by rewrite lookup_empty. Qed.
 Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
 Proof.
@@ -319,9 +321,10 @@ Proof.
 Qed.
 
 (** ** Properties of the [alter] operation *)
-Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <$> m !! i.
+Lemma lookup_alter {A} (f : A → A) (m : M A) i : alter f i m !! i = f <$> m !! i.
 Proof. unfold alter. apply lookup_partial_alter. Qed.
-Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠ j → alter f i m !! j = m !! j.
+Lemma lookup_alter_ne {A} (f : A → A) (m : M A) i j :
+  i ≠ j → alter f i m !! j = m !! j.
 Proof. unfold alter. apply lookup_partial_alter_ne. Qed.
 Lemma alter_ext {A} (f g : A → A) (m : M A) i :
   (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
@@ -335,7 +338,7 @@ Qed.
 Lemma alter_commute {A} (f g : A → A) (m : M A) i j :
   i ≠ j → alter f i (alter g j m) = alter g j (alter f i m).
 Proof. apply partial_alter_commute. Qed.
-Lemma lookup_alter_Some {A} (f : A → A) m i j y :
+Lemma lookup_alter_Some {A} (f : A → A) (m : M A) i j y :
   alter f i m !! j = Some y ↔
     (i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠ j ∧ m !! j = Some y).
 Proof.
@@ -343,16 +346,16 @@ Proof.
   - rewrite lookup_alter. naive_solver (simplify_option_eq; eauto).
   - rewrite lookup_alter_ne by done. naive_solver.
 Qed.
-Lemma lookup_alter_None {A} (f : A → A) m i j :
+Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
   alter f i m !! j = None ↔ m !! j = None.
 Proof.
   by destruct (decide (i = j)) as [->|?];
     rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne.
 Qed.
-Lemma lookup_alter_is_Some {A} (f : A → A) m i j :
+Lemma lookup_alter_is_Some {A} (f : A → A) (m : M A) i j :
   is_Some (alter f i m !! j) ↔ is_Some (m !! j).
 Proof. by rewrite <-!not_eq_None_Some, lookup_alter_None. Qed.
-Lemma alter_id {A} (f : A → A) m i :
+Lemma alter_id {A} (f : A → A) (m : M A) i :
   (∀ x, m !! i = Some x → f x = x) → alter f i m = m.
 Proof.
   intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?].
@@ -484,7 +487,7 @@ Proof.
   - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
   - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
 Qed.
-Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}.
+Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}.
 Proof. done. Qed.
 Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅.
 Proof.
@@ -542,44 +545,47 @@ Qed.
 
 (** ** Properties of the singleton maps *)
 Lemma lookup_singleton_Some {A} i j (x y : A) :
-  {[i := x]} !! j = Some y ↔ i = j ∧ x = y.
+  ({[i := x]} : M A) !! j = Some y ↔ i = j ∧ x = y.
 Proof.
   rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence.
 Qed.
-Lemma lookup_singleton_None {A} i j (x : A) : {[i := x]} !! j = None ↔ i ≠ j.
+Lemma lookup_singleton_None {A} i j (x : A) :
+  ({[i := x]} : M A) !! j = None ↔ i ≠ j.
 Proof. rewrite <-insert_empty,lookup_insert_None, lookup_empty; tauto. Qed.
-Lemma lookup_singleton {A} i (x : A) : {[i := x]} !! i = Some x.
+Lemma lookup_singleton {A} i (x : A) : ({[i := x]} : M A) !! i = Some x.
 Proof. by rewrite lookup_singleton_Some. Qed.
-Lemma lookup_singleton_ne {A} i j (x : A) : i ≠ j → {[i := x]} !! j = None.
+Lemma lookup_singleton_ne {A} i j (x : A) :
+  i ≠ j → ({[i := x]} : M A) !! j = None.
 Proof. by rewrite lookup_singleton_None. Qed.
-Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ ∅.
+Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A).
 Proof.
   intros Hix. apply (f_equal (!! i)) in Hix.
   by rewrite lookup_empty, lookup_singleton in Hix.
 Qed.
-Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i := x]} = {[i := y]}.
+Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}.
 Proof.
   unfold singletonM, map_singleton, insert, map_insert.
   by rewrite <-partial_alter_compose.
 Qed.
-Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i := x]} = {[i := f x]}.
+Lemma alter_singleton {A} (f : A → A) i x :
+  alter f i ({[i := x]} : M A) = {[i := f x]}.
 Proof.
   intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
   - by rewrite lookup_alter, !lookup_singleton.
   - by rewrite lookup_alter_ne, !lookup_singleton_ne.
 Qed.
 Lemma alter_singleton_ne {A} (f : A → A) i j x :
-  i ≠ j → alter f i {[j := x]} = {[j := x]}.
+  i ≠ j → alter f i ({[j := x]} : M A) = {[j := x]}.
 Proof.
   intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
     rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
 Qed.
-Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ ∅.
+Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ (∅ : M A).
 Proof. apply insert_non_empty. Qed.
-Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = ∅.
+Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = (∅ : M A).
 Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
 Lemma delete_singleton_ne {A} i j (x : A) :
-  i ≠ j → delete i {[j := x]} = {[j := x]}.
+  i ≠ j → delete i ({[j := x]} : M A) = {[j := x]}.
 Proof. intro. apply delete_notin. by apply lookup_singleton_ne. Qed.
 
 (** ** Properties of the map operations *)
@@ -621,19 +627,19 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
   g ∘ f <$> m = g <$> f <$> m.
 Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
-Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m :
+Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) (m : M A) :
   (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
 Proof.
   intros Hi i; rewrite !lookup_fmap.
   destruct (m !! i) eqn:?; constructor; eauto.
 Qed.
-Lemma map_fmap_ext {A B} (f1 f2 : A → B) m :
+Lemma map_fmap_ext {A B} (f1 f2 : A → B) (m : M A) :
   (∀ i x, m !! i = Some x → f1 x = f2 x) → f1 <$> m = f2 <$> m.
 Proof.
   intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
   by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
 Qed.
-Lemma omap_ext {A B} (f1 f2 : A → option B) m :
+Lemma omap_ext {A B} (f1 f2 : A → option B) (m : M A) :
   (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m.
 Proof.
   intros Hi; apply map_eq; intros i; rewrite !lookup_omap.
@@ -670,7 +676,7 @@ Proof. rewrite !elem_of_map_to_list. congruence. Qed.
 Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1).
 Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
 Lemma elem_of_map_of_list_1' {A} (l : list (K * A)) i x :
-  (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → map_of_list l !! i = Some x.
+  (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x.
 Proof.
   induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
   setoid_rewrite elem_of_cons.
@@ -680,7 +686,7 @@ Proof.
   - rewrite lookup_insert_ne by done; eauto.
 Qed.
 Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
-  NoDup (l.*1) → (i,x) ∈ l → map_of_list l !! i = Some x.
+  NoDup (l.*1) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x.
 Proof.
   intros ? Hx; apply elem_of_map_of_list_1'; eauto using NoDup_fmap_fst.
   intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
@@ -688,7 +694,7 @@ Proof.
     by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
 Qed.
 Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x :
-  map_of_list l !! i = Some x → (i,x) ∈ l.
+  (map_of_list l : M A) !! i = Some x → (i,x) ∈ l.
 Proof.
   induction l as [|[j y] l IH]; simpl; [by rewrite lookup_empty|].
   rewrite elem_of_cons. destruct (decide (i = j)) as [->|];
@@ -696,20 +702,20 @@ Proof.
 Qed.
 Lemma elem_of_map_of_list' {A} (l : list (K * A)) i x :
   (∀ x', (i,x) ∈ l → (i,x') ∈ l → x = x') →
-  (i,x) ∈ l ↔ map_of_list l !! i = Some x.
+  (i,x) ∈ l ↔ (map_of_list l : M A) !! i = Some x.
 Proof. split; auto using elem_of_map_of_list_1', elem_of_map_of_list_2. Qed.
 Lemma elem_of_map_of_list {A} (l : list (K * A)) i x :
-  NoDup (l.*1) → (i,x) ∈ l ↔ map_of_list l !! i = Some x.
+  NoDup (l.*1) → (i,x) ∈ l ↔ (map_of_list l : M A) !! i = Some x.
 Proof. split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. Qed.
 
 Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
-  i ∉ l.*1 → map_of_list l !! i = None.
+  i ∉ l.*1 → (map_of_list l : M A) !! i = None.
 Proof.
   rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
   exists (i,x); simpl; auto using elem_of_map_of_list_2.
 Qed.
 Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
-  map_of_list l !! i = None → i ∉ l.*1.
+  (map_of_list l : M A) !! i = None → i ∉ l.*1.
 Proof.
   induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
   rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq.
@@ -717,16 +723,17 @@ Proof.
   - by rewrite lookup_insert_ne; intuition.
 Qed.
 Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
-  i ∉ l.*1 ↔ map_of_list l !! i = None.
+  i ∉ l.*1 ↔ (map_of_list l : M A) !! i = None.
 Proof. red; auto using not_elem_of_map_of_list_1,not_elem_of_map_of_list_2. Qed.
 Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) :
-  NoDup (l1.*1) → l1 ≡ₚ l2 → map_of_list l1 = map_of_list l2.
+  NoDup (l1.*1) → l1 ≡ₚ l2 → (map_of_list l1 : M A) = map_of_list l2.
 Proof.
   intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
   by rewrite <-!elem_of_map_of_list; rewrite <-?Hperm.
 Qed.
 Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
-  NoDup (l1.*1) → NoDup (l2.*1) → map_of_list l1 = map_of_list l2 → l1 ≡ₚ l2.
+  NoDup (l1.*1) → NoDup (l2.*1) →
+  (map_of_list l1 : M A) = map_of_list l2 → l1 ≡ₚ l2.
 Proof.
   intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
   intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
@@ -753,13 +760,13 @@ Proof.
   auto using map_of_list_proper, NoDup_fst_map_to_list.
 Qed.
 
-Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
+Lemma map_of_list_nil {A} : map_of_list [] = (∅ : M A).
 Proof. done. Qed.
 Lemma map_of_list_cons {A} (l : list (K * A)) i x :
-  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l).
+  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l : M A).
 Proof. done. Qed.
 Lemma map_of_list_fmap {A B} (f : A → B) l :
-  map_of_list (prod_map id f <$> l) = f <$> map_of_list l.
+  map_of_list (prod_map id f <$> l) = f <$> (map_of_list l : M A).
 Proof.
   induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto.
   rewrite <-map_of_list_cons; simpl. by rewrite IH, <-fmap_insert.
@@ -780,7 +787,8 @@ Proof.
     rewrite elem_of_map_to_list in Hlookup. congruence.
   - by rewrite !map_of_to_list.
 Qed.
-Lemma map_to_list_singleton {A} i (x : A) : map_to_list {[i:=x]} = [(i,x)].
+Lemma map_to_list_singleton {A} i (x : A) :
+  map_to_list ({[i:=x]} : M A) = [(i,x)].
 Proof.
   apply Permutation_singleton. unfold singletonM, map_singleton.
   by rewrite map_to_list_insert, map_to_list_empty by auto using lookup_empty.
@@ -792,7 +800,7 @@ Proof.
   intros; apply NoDup_submseteq; auto using NoDup_map_to_list.
   intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
 Qed.
-Lemma map_to_list_fmap {A B} (f : A → B) m :
+Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) :
   map_to_list (f <$> m) ≡ₚ prod_map id f <$> map_to_list m.
 Proof.
   assert (NoDup ((prod_map id f <$> map_to_list m).*1)).
@@ -836,7 +844,7 @@ Proof.
 Defined.
 
 (** Properties of the imap function *)
-Lemma lookup_imap {A B} (f : K → A → option B) m i :
+Lemma lookup_imap {A B} (f : K → A → option B) (m : M A) i :
   map_imap f m !! i = m !! i ≫= f i.
 Proof.
   unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
@@ -856,9 +864,9 @@ Qed.
 Section map_of_to_collection.
   Context {A : Type} `{FinCollection B C}.
 
-  Lemma lookup_map_of_collection (f : B → K * A) Y i x :
+  Lemma lookup_map_of_collection (f : B → K * A) (Y : C) i x :
     (∀ y y', y ∈ Y → y' ∈ Y → (f y).1 = (f y').1 → y = y') →
-    map_of_collection f Y !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x).
+    (map_of_collection f Y : M A) !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x).
   Proof.
     intros Hinj. assert (∀ x',
       (i, x) ∈ f <$> elements Y → (i, x') ∈ f <$> elements Y → x = x').
@@ -870,14 +878,15 @@ Section map_of_to_collection.
   Qed.
 
   Lemma elem_of_map_to_collection (f : K → A → B) (m : M A) (y : B) :
-    y ∈ map_to_collection f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
+    y ∈ map_to_collection (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
   Proof.
     unfold map_to_collection; simpl.
     rewrite elem_of_of_list, elem_of_list_fmap. split.
     - intros ([i x] & ? & ?%elem_of_map_to_list); eauto.
     - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list.
   Qed.
-  Lemma map_to_collection_empty (f : K → A → B) : map_to_collection f ∅ = ∅.
+  Lemma map_to_collection_empty (f : K → A → B) :
+    map_to_collection f (∅ : M A) = (∅ : C).
   Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed.
   Lemma map_to_collection_insert (f : K → A → B)(m : M A) i x :
     m !! i = None →
@@ -885,7 +894,7 @@ Section map_of_to_collection.
   Proof.
     intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert.
   Qed.
-  Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) m i x :
+  Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x :
     m !! i = None →
     map_to_collection (C:=C) f (<[i:=x]>m) = {[f i x]} ∪ map_to_collection f m.
   Proof. unfold_leibniz. apply map_to_collection_insert. Qed.
@@ -893,7 +902,7 @@ End map_of_to_collection.
 
 Lemma lookup_map_of_collection_id `{FinCollection (K * A) C} (X : C) i x :
   (∀ i y y', (i,y) ∈ X → (i,y') ∈ X → y = y') →
-  map_of_collection id X !! i = Some x ↔ (i,x) ∈ X.
+  (map_of_collection id X : M A) !! i = Some x ↔ (i,x) ∈ X.
 Proof.
   intros. etrans; [apply lookup_map_of_collection|naive_solver].
   intros [] [] ???; simplify_eq/=; eauto with f_equal.
@@ -996,6 +1005,7 @@ Qed.
 (** ** Properties of the [map_Forall] predicate *)
 Section map_Forall.
 Context {A} (P : K → A → Prop).
+Implicit Types m : M A.
 
 Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
 Proof.
@@ -1003,7 +1013,7 @@ Proof.
   - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
   - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
 Qed.
-Lemma map_Forall_empty : map_Forall P ∅.
+Lemma map_Forall_empty : map_Forall P (∅ : M A).
 Proof. intros i x. by rewrite lookup_empty. Qed.
 Lemma map_Forall_impl (Q : K → A → Prop) m :
   map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
@@ -1052,12 +1062,14 @@ End map_Forall.
 (** ** Properties of the [merge] operation *)
 Section merge.
 Context {A} (f : option A → option A → option A) `{!DiagNone f}.
-Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
+Implicit Types m : M A.
+
+Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f).
 Proof.
   intros ??. apply map_eq. intros.
   by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
 Qed.
-Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
+Global Instance: RightId (=) None f → RightId (=) (∅ : M A) (merge f).
 Proof.
   intros ??. apply map_eq. intros.
   by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
@@ -1066,34 +1078,34 @@ Lemma merge_comm m1 m2 :
   (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
   merge f m1 m2 = merge f m2 m1.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_comm' : Comm (=) f → Comm (=) (merge f).
+Global Instance merge_comm' : Comm (=) f → Comm (=) (merge (M:=M) f).
 Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
 Lemma merge_assoc m1 m2 m3 :
   (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
         f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
   merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge f).
+Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge (M:=M) f).
 Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
 Lemma merge_idemp m1 :
   (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge f).
+Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge (M:=M) f).
 Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
 End merge.
 
 Section more_merge.
 Context {A B C} (f : option A → option B → option C) `{!DiagNone f}.
 
-Lemma merge_Some m1 m2 m :
+Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) :
   (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
 Proof.
   split; [|intros <-; apply (lookup_merge _) ].
   intros Hlookup. apply map_eq; intros. rewrite Hlookup. apply (lookup_merge _).
 Qed.
-Lemma merge_empty : merge f ∅ ∅ = ∅.
+Lemma merge_empty : merge f (∅ : M A) (∅ : M B) = ∅.
 Proof. apply map_eq. intros. by rewrite !(lookup_merge f), !lookup_empty. Qed.
-Lemma partial_alter_merge g g1 g2 m1 m2 i :
+Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i :
   g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) →
   partial_alter g i (merge f m1 m2) =
     merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
@@ -1102,7 +1114,7 @@ Proof.
   - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
   - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
 Qed.
-Lemma partial_alter_merge_l g g1 m1 m2 i :
+Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) i :
   g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
   partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
 Proof.
@@ -1110,7 +1122,7 @@ Proof.
   - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
   - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
 Qed.
-Lemma partial_alter_merge_r g g2 m1 m2 i :
+Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) i :
   g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
   partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
 Proof.
@@ -1118,37 +1130,39 @@ Proof.
   - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
   - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
 Qed.
-Lemma insert_merge m1 m2 i x y z :
+Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
   f (Some y) (Some z) = Some x →
   <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
 Proof. by intros; apply partial_alter_merge. Qed.
 Lemma merge_singleton i x y z :
-  f (Some y) (Some z) = Some x → merge f {[i := y]} {[i := z]} = {[i := x]}.
+  f (Some y) (Some z) = Some x →
+  merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}.
 Proof.
   intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
 Qed.
-Lemma insert_merge_l m1 m2 i x y :
+Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y :
   f (Some y) (m2 !! i) = Some x →
   <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) m2.
 Proof. by intros; apply partial_alter_merge_l. Qed.
-Lemma insert_merge_r m1 m2 i x z :
+Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z :
   f (m1 !! i) (Some z) = Some x →
   <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
 Proof. by intros; apply partial_alter_merge_r. Qed.
 End more_merge.
 
 (** Properties of the zip_with function *)
-Lemma map_lookup_zip_with {A B C} (f : A → B → C) m1 m2 i :
+Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
   map_zip_with f m1 m2 !! i = x ← m1 !! i; y ← m2 !! i; Some (f x y).
 Proof.
   unfold map_zip_with. rewrite lookup_merge by done.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
 
-Lemma map_zip_with_empty {A B C} (f : A → B → C) : map_zip_with f ∅ ∅ = ∅.
+Lemma map_zip_with_empty {A B C} (f : A → B → C) :
+  map_zip_with f (∅ : M A) (∅ : M B) = ∅.
 Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
 
-Lemma map_insert_zip_with {A B C} (f : A → B → C) m1 m2 i x y z :
+Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i x y z :
   f y z = x →
   <[i:=x]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
 Proof.
@@ -1157,7 +1171,7 @@ Proof.
 Qed.
 
 Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C)
-    (g1 : A' → A) (g2 : B' → B) m1 m2 :
+    (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') :
   map_zip_with f (g1 <$> m1) (g2 <$> m2) = map_zip_with (λ x y, f (g1 x) (g2 y)) m1 m2.
 Proof.
   apply map_eq; intro i. rewrite !map_lookup_zip_with, !lookup_fmap.
@@ -1165,13 +1179,14 @@ Proof.
 Qed.
 
 Lemma map_zip_with_fmap_1 {A' A B C} (f : A → B → C)
-      (g : A' → A) m1 m2 :
+    (g : A' → A) (m1 : M A') (m2 : M B) :
   map_zip_with f (g <$> m1) m2 = map_zip_with (λ x y, f (g x) y) m1 m2.
 Proof.
   rewrite <- (map_fmap_id m2) at 1. by rewrite map_zip_with_fmap. 
 Qed.
 
-Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C) (g : B' → B) m1 m2 :
+Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C)
+    (g : B' → B) (m1 : M A) (m2 : M B') :
   map_zip_with f m1 (g <$> m2) = map_zip_with (λ x y, f x (g y)) m1 m2.
 Proof.
   rewrite <- (map_fmap_id m1) at 1. by rewrite map_zip_with_fmap.
@@ -1184,14 +1199,15 @@ Proof.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
 
-Lemma map_zip_with_map_zip {A B C} (f : A → B → C) m1 m2 :
+Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
   map_zip_with f m1 m2 = curry f <$> map_zip m1 m2.
 Proof.
   apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
 
-Lemma map_fmap_zip {A' A B' B} (g1 : A' → A) (g2 : B' → B) m1 m2 :
+Lemma map_fmap_zip {A' A B' B} (g1 : A' → A)
+    (g2 : B' → B) (m1 : M A') (m2 : M B') :
   map_zip (fmap g1 m1) (fmap g2 m2) = prod_map g1 g2 <$> map_zip m1 m2.
 Proof.
   rewrite map_zip_with_fmap, map_zip_with_map_zip.
@@ -1223,7 +1239,7 @@ Proof.
       by eapply bool_decide_unpack, Hm.
 Qed.
 Global Instance map_relation_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x),
-  ∀ y, Decision (Q y)} m1 m2 : Decision (map_relation R P Q m1 m2).
+  ∀ y, Decision (Q y)} (m1 : M A) (m2 : M B) : Decision (map_relation R P Q m1 m2).
 Proof.
   refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
     abstract by rewrite map_relation_alt.
@@ -1316,6 +1332,7 @@ Proof. symmetry. by apply map_disjoint_delete_l. Qed.
 (** ** Properties of the [union_with] operation *)
 Section union_with.
 Context {A} (f : A → A → option A).
+Implicit Types m : M A.
 
 Lemma lookup_union_with m1 m2 i :
   union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
@@ -1659,10 +1676,10 @@ Lemma map_disjoint_of_list_zip_r_2 {A} (m : M A) is xs :
 Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
 
 (** ** Properties of the [intersection_with] operation *)
-Lemma lookup_intersection_with {A} (f : A → A → option A) m1 m2 i :
+Lemma lookup_intersection_with {A} (f : A → A → option A) (m1 m2 : M A) i :
   intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
 Proof. by rewrite <-(lookup_merge _). Qed.
-Lemma lookup_intersection_with_Some {A} (f : A → A → option A) m1 m2 i z :
+Lemma lookup_intersection_with_Some {A} (f : A → A → option A) (m1 m2 : M A) i z :
   intersection_with f m1 m2 !! i = Some z ↔
     (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
 Proof.
@@ -1685,10 +1702,10 @@ Proof.
 Qed.
 
 (** ** Properties of the [difference_with] operation *)
-Lemma lookup_difference_with {A} (f : A → A → option A) m1 m2 i :
+Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i :
   difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i).
 Proof. by rewrite <-lookup_merge by done. Qed.
-Lemma lookup_difference_with_Some {A} (f : A → A → option A) m1 m2 i z :
+Lemma lookup_difference_with_Some {A} (f : A → A → option A) (m1 m2 : M A) i z :
   difference_with f m1 m2 !! i = Some z ↔
     (m1 !! i = Some z ∧ m2 !! i = None) ∨
     (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
diff --git a/theories/gmap.v b/theories/gmap.v
index fe7ddf77..874fff96 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -136,8 +136,10 @@ Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
 Section curry_uncurry.
   Context `{Countable K1, Countable K2} {A : Type}.
 
+  (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
+  a consequence of Coq bug #5735 *)
   Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
-    gmap_curry m !! (i,j) = m !! i ≫= (!! j).
+    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (!! j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (!! j))).
     { by rewrite !lookup_empty. }
@@ -154,7 +156,7 @@ Section curry_uncurry.
   Qed.
 
   Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
-    gmap_uncurry m !! i ≫= (!! j) = m !! (i, j).
+    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (!! j) = m !! (i, j).
   Proof.
     apply (map_fold_ind (λ mr m, mr !! i ≫= (!! j) = m !! (i, j))).
     { by rewrite !lookup_empty. }
@@ -229,7 +231,7 @@ Qed.
 (* This is pretty ad-hoc and just for the case of [gset positive]. We need a
 notion of countable non-finite types to generalize this. *)
 Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
-  let 'Mapset (GMap m _) := X in fresh (dom _ m).
+  let 'Mapset (GMap m _) := X in fresh (dom Pset m).
 Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
 Proof.
   split.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 084dfdca..f61416e9 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -25,27 +25,27 @@ Section definitions.
 
   Definition multiplicity (x : A) (X : gmultiset A) : nat :=
     match gmultiset_car X !! x with Some n => S n | None => 0 end.
-  Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
+  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
     0 < multiplicity x X.
-  Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
+  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
     multiplicity x X ≤ multiplicity x Y.
 
-  Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
+  Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
     let (X) := X in '(x,n) ← map_to_list X; replicate (S n) x.
-  Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
+  Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
 
-  Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
-  Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
+  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
+  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
     GMultiSet {[ x := 0 ]}.
-  Instance gmultiset_union : Union (gmultiset A) := λ X Y,
+  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
     let (X) := X in let (Y) := Y in
     GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
-  Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
+  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
     let (X) := X in let (Y) := Y in
     GMultiSet $ difference_with (λ x y,
       let z := x - y in guard (0 < z); Some (pred z)) X Y.
 
-  Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
+  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
     let (X) := X in dom _ X.
 End definitions.
 
@@ -54,27 +54,6 @@ Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
 Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
 Typeclasses Opaque gmultiset_dom.
 
-(** These instances are declared using [Hint Extern] to avoid too
-eager type class search. *)
-Hint Extern 1 (ElemOf _ (gmultiset _)) =>
-  eapply @gmultiset_elem_of : typeclass_instances.
-Hint Extern 1 (SubsetEq (gmultiset _)) =>
-  eapply @gmultiset_subseteq : typeclass_instances.
-Hint Extern 1 (Empty (gmultiset _)) =>
-  eapply @gmultiset_empty : typeclass_instances.
-Hint Extern 1 (Singleton _ (gmultiset _)) =>
-  eapply @gmultiset_singleton : typeclass_instances.
-Hint Extern 1 (Union (gmultiset _)) =>
-  eapply @gmultiset_union : typeclass_instances.
-Hint Extern 1 (Difference (gmultiset _)) =>
-  eapply @gmultiset_difference : typeclass_instances.
-Hint Extern 1 (Elements _ (gmultiset _)) =>
-  eapply @gmultiset_elements : typeclass_instances.
-Hint Extern 1 (Size (gmultiset _)) =>
-  eapply @gmultiset_size : typeclass_instances.
-Hint Extern 1 (Dom (gmultiset _) _) =>
-  eapply @gmultiset_dom : typeclass_instances.
-
 Section lemmas.
 Context `{Countable A}.
 Implicit Types x y : A.
diff --git a/theories/hashset.v b/theories/hashset.v
index 59c5506b..20a7d4ae 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -18,18 +18,18 @@ Arguments hashset_car {_ _} _ : assert.
 Section hashset.
 Context `{EqDecision A} (hash : A → Z).
 
-Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
+Global Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
   hashset_car m !! hash x = Some l ∧ x ∈ l.
 
-Program Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _.
+Global Program Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _.
 Next Obligation. by intros n X; simpl_map. Qed.
-Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
+Global Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
   Hashset {[ hash x := [x] ]} _.
 Next Obligation.
   intros x n l [<- <-]%lookup_singleton_Some.
   rewrite Forall_singleton; auto using NoDup_singleton.
 Qed.
-Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
+Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. 
 Next Obligation.
@@ -38,7 +38,7 @@ Next Obligation.
   split; [apply Forall_list_union|apply NoDup_list_union];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
 Qed.
-Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
+Global Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (intersection_with (λ l k,
     let l' := list_intersection l k in guard (l' ≠ []); Some l') m1 m2) _.
@@ -48,7 +48,7 @@ Next Obligation.
   split; [apply Forall_list_intersection|apply NoDup_list_intersection];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
 Qed.
-Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
+Global Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (difference_with (λ l k,
     let l' := list_difference l k in guard (l' ≠ []); Some l') m1 m2) _.
@@ -58,10 +58,10 @@ Next Obligation.
   split; [apply Forall_list_difference|apply NoDup_list_difference];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
 Qed.
-Instance hashset_elems: Elements A (hashset hash) := λ m,
+Global Instance hashset_elements: Elements A (hashset hash) := λ m,
   map_to_list (hashset_car m) ≫= snd.
 
-Global Instance: FinCollection A (hashset hash).
+Global Instance hashset_fin_collection : FinCollection A (hashset hash).
 Proof.
   split; [split; [split| |]| |].
   - intros ? (?&?&?); simplify_map_eq/=.
@@ -98,13 +98,13 @@ Proof.
     assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
     exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
-  - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
+  - unfold elem_of at 2, hashset_elem_of, elements, hashset_elements.
     intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
     { intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn.
       cut (hash x = n); [intros <-; eauto|].
       eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. }
     intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
-  - unfold elements, hashset_elems. intros [m Hm]; simpl.
+  - unfold elements, hashset_elements. intros [m Hm]; simpl.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??]];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
@@ -120,23 +120,6 @@ End hashset.
 
 Typeclasses Opaque hashset_elem_of.
 
-(** These instances are declared using [Hint Extern] to avoid too
-eager type class search. *)
-Hint Extern 1 (ElemOf _ (hashset _)) =>
-  eapply @hashset_elem_of : typeclass_instances.
-Hint Extern 1 (Empty (hashset _)) =>
-  eapply @hashset_empty : typeclass_instances.
-Hint Extern 1 (Singleton _ (hashset _)) =>
-  eapply @hashset_singleton : typeclass_instances.
-Hint Extern 1 (Union (hashset _)) =>
-  eapply @hashset_union : typeclass_instances.
-Hint Extern 1 (Intersection (hashset _)) =>
-  eapply @hashset_intersection : typeclass_instances.
-Hint Extern 1 (Difference (hashset _)) =>
-  eapply @hashset_difference : typeclass_instances.
-Hint Extern 1 (Elements _ (hashset _)) =>
-  eapply @hashset_elems : typeclass_instances.
-
 Section remove_duplicates.
 Context `{EqDecision A} (hash : A → Z).
 
diff --git a/theories/list.v b/theories/list.v
index 5f3bf784..a258bea8 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 →
 
 Section list_set.
   Context `{dec : EqDecision A}.
-  Global Instance elem_of_list_dec (x : A) : ∀ l, Decision (x ∈ l).
+  Global Instance elem_of_list_dec (x : A) : ∀ l : list A, Decision (x ∈ l).
   Proof.
    refine (
     fix go l :=
@@ -2857,6 +2857,7 @@ Proof. induction l; f_equal/=; auto. Qed.
 
 Section fmap.
   Context {A B : Type} (f : A → B).
+  Implicit Types l : list A.
 
   Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
   Proof. induction l; f_equal/=; auto. Qed.
@@ -2975,24 +2976,24 @@ Section fmap.
   Lemma Exists_fmap (P : B → Prop) l : Exists P (f <$> l) ↔ Exists (P ∘ f) l.
   Proof. split; induction l; inversion 1; constructor; by auto. Qed.
 
-  Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
-    Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
+  Lemma Forall2_fmap_l {C} (P : B → C → Prop) l k :
+    Forall2 P (f <$> l) k ↔ Forall2 (P ∘ f) l k.
   Proof.
-    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
+    split; revert k; induction l; inversion_clear 1; constructor; auto.
   Qed.
-  Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 :
-    Forall2 P l1 (f <$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2.
+  Lemma Forall2_fmap_r {C} (P : C → B → Prop) k l :
+    Forall2 P k (f <$> l) ↔ Forall2 (λ x, P x ∘ f) k l.
   Proof.
-    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+    split; revert k; induction l; inversion_clear 1; constructor; auto.
   Qed.
-  Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
-    Forall2 P (f <$> l1) (g <$> l2) → Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
-  Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
-  Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
-    Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 → Forall2 P (f <$> l1) (g <$> l2).
+  Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l k :
+    Forall2 P (f <$> l) (g <$> k) → Forall2 (λ x1 x2, P (f x1) (g x2)) l k.
+  Proof. revert k; induction l; intros [|??]; inversion_clear 1; auto. Qed.
+  Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l k :
+    Forall2 (λ x1 x2, P (f x1) (g x2)) l k → Forall2 P (f <$> l) (g <$> k).
   Proof. induction 1; csimpl; auto. Qed.
-  Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
-    Forall2 P (f <$> l1) (g <$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
+  Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l k :
+    Forall2 P (f <$> l) (g <$> k) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l k.
   Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
 
   Lemma list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
@@ -3081,7 +3082,7 @@ Section ret_join.
   Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
   Proof. apply elem_of_list_singleton. Qed.
   Lemma elem_of_list_join (x : A) (ls : list (list A)) :
-    x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls.
+    x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls.
   Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
   Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (= []) ls.
   Proof.
diff --git a/theories/listset.v b/theories/listset.v
index 4649ede5..824cbc45 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -12,14 +12,14 @@ Arguments Listset {_} _ : assert.
 Section listset.
 Context {A : Type}.
 
-Instance listset_elem_of: ElemOf A (listset A) := λ x l, x ∈ listset_car l.
-Instance listset_empty: Empty (listset A) := Listset [].
-Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
-Instance listset_union: Union (listset A) := λ l k,
+Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, x ∈ listset_car l.
+Global Instance listset_empty: Empty (listset A) := Listset [].
+Global Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
+Global Instance listset_union: Union (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (l' ++ k').
 Global Opaque listset_singleton listset_empty.
 
-Global Instance: SimpleCollection A (listset A).
+Global Instance listset_simple_collection : SimpleCollection A (listset A).
 Proof.
   split.
   - by apply not_elem_of_nil.
@@ -40,20 +40,21 @@ Defined.
 
 Context `{!EqDecision A}.
 
-Instance listset_intersection: Intersection (listset A) := λ l k,
+Global Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').
-Instance listset_difference: Difference (listset A) := λ l k,
+Global Instance listset_difference: Difference (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_difference l' k').
 
-Instance: Collection A (listset A).
+Instance listset_collection: Collection A (listset A).
 Proof.
   split.
   - apply _.
   - intros [?] [?]. apply elem_of_list_intersection.
   - intros [?] [?]. apply elem_of_list_difference.
 Qed.
-Instance listset_elems: Elements A (listset A) := remove_dups ∘ listset_car.
-Global Instance: FinCollection A (listset A).
+Global Instance listset_elements: Elements A (listset A) :=
+  remove_dups ∘ listset_car.
+Global Instance listset_fin_collection : FinCollection A (listset A).
 Proof.
   split.
   - apply _.
@@ -62,23 +63,6 @@ Proof.
 Qed.
 End listset.
 
-(** These instances are declared using [Hint Extern] to avoid too
-eager type class search. *)
-Hint Extern 1 (ElemOf _ (listset _)) =>
-  eapply @listset_elem_of : typeclass_instances.
-Hint Extern 1 (Empty (listset _)) =>
-  eapply @listset_empty : typeclass_instances.
-Hint Extern 1 (Singleton _ (listset _)) =>
-  eapply @listset_singleton : typeclass_instances.
-Hint Extern 1 (Union (listset _)) =>
-  eapply @listset_union : typeclass_instances.
-Hint Extern 1 (Intersection (listset _)) =>
-  eapply @listset_intersection : typeclass_instances.
-Hint Extern 1 (Difference (listset _)) =>
-  eapply @listset_difference : typeclass_instances.
-Hint Extern 1 (Elements _ (listset _)) =>
-  eapply @listset_elems : typeclass_instances.
-
 Instance listset_ret: MRet listset := λ A x, {[ x ]}.
 Instance listset_fmap: FMap listset := λ A B f l,
   let (l') := l in Listset (f <$> l').
@@ -86,7 +70,7 @@ Instance listset_bind: MBind listset := λ A B f l,
   let (l') := l in Listset (mbind (listset_car ∘ f) l').
 Instance listset_join: MJoin listset := λ A, mbind id.
 
-Instance: CollectionMonad listset.
+Instance listset_collection_monad : CollectionMonad listset.
 Proof.
   split.
   - intros. apply _.
diff --git a/theories/mapset.v b/theories/mapset.v
index bb44b671..bb7c479d 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -14,18 +14,18 @@ Arguments mapset_car {_} _ : assert.
 Section mapset.
 Context `{FinMap K M}.
 
-Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
+Global Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
   mapset_car X !! x = Some ().
-Instance mapset_empty: Empty (mapset M) := Mapset ∅.
-Instance mapset_singleton: Singleton K (mapset M) := λ x,
+Global Instance mapset_empty: Empty (mapset M) := Mapset ∅.
+Global Instance mapset_singleton: Singleton K (mapset M) := λ x,
   Mapset {[ x := () ]}.
-Instance mapset_union: Union (mapset M) := λ X1 X2,
+Global Instance mapset_union: Union (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
-Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
+Global Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
-Instance mapset_difference: Difference (mapset M) := λ X1 X2,
+Global Instance mapset_difference: Difference (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
-Instance mapset_elems: Elements K (mapset M) := λ X,
+Global Instance mapset_elements: Elements K (mapset M) := λ X,
   let (m) := X in (map_to_list m).*1.
 
 Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
@@ -35,7 +35,7 @@ Proof.
   f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
 Qed.
 
-Instance: Collection K (mapset M).
+Instance mapset_collection: Collection K (mapset M).
 Proof.
   split; [split | | ].
   - unfold empty, elem_of, mapset_empty, mapset_elem_of.
@@ -54,17 +54,17 @@ Proof.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
 Qed.
-Global Instance: LeibnizEquiv (mapset M).
+Global Instance mapset_leibniz : LeibnizEquiv (mapset M).
 Proof. intros ??. apply mapset_eq. Qed.
-Global Instance: FinCollection K (mapset M).
+Global Instance mapset_fin_collection : FinCollection K (mapset M).
 Proof.
   split.
   - apply _.
-  - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
+  - unfold elements, elem_of at 2, mapset_elements, mapset_elem_of.
     intros [m] x. simpl. rewrite elem_of_list_fmap. split.
     + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
     + intros. exists (x, ()). by rewrite elem_of_map_to_list.
-  - unfold elements, mapset_elems. intros [m]. simpl.
+  - unfold elements, mapset_elements. intros [m]. simpl.
     apply NoDup_fst_map_to_list.
 Qed.
 
@@ -127,21 +127,4 @@ Proof.
 Qed.
 End mapset.
 
-(** These instances are declared using [Hint Extern] to avoid too
-eager type class search. *)
-Hint Extern 1 (ElemOf _ (mapset _)) =>
-  eapply @mapset_elem_of : typeclass_instances.
-Hint Extern 1 (Empty (mapset _)) =>
-  eapply @mapset_empty : typeclass_instances.
-Hint Extern 1 (Singleton _ (mapset _)) =>
-  eapply @mapset_singleton : typeclass_instances.
-Hint Extern 1 (Union (mapset _)) =>
-  eapply @mapset_union : typeclass_instances.
-Hint Extern 1 (Intersection (mapset _)) =>
-  eapply @mapset_intersection : typeclass_instances.
-Hint Extern 1 (Difference (mapset _)) =>
-  eapply @mapset_difference : typeclass_instances.
-Hint Extern 1 (Elements _ (mapset _)) =>
-  eapply @mapset_elems : typeclass_instances.
-
 Arguments mapset_eq_dec : simpl never.
diff --git a/theories/option.v b/theories/option.v
index 7a2c27f9..9f5b7efb 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -207,7 +207,7 @@ Proof. by destruct mx. Qed.
 Lemma option_fmap_ext {A B} (f g : A → B) mx :
   (∀ x, f x = g x) → f <$> mx = g <$> mx.
 Proof. intros; destruct mx; f_equal/=; auto. Qed.
-Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) mx :
+Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) (mx : option A) :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
@@ -306,13 +306,15 @@ Section union_intersection_difference.
   Proof. by intros [?|]. Qed.
   Global Instance union_with_right_id : RightId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
-  Global Instance union_with_comm : Comm (=) f → Comm (=) (union_with f).
+  Global Instance union_with_comm :
+    Comm (=) f → Comm (=) (union_with (M:=option A) f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
   Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
-  Global Instance difference_with_comm : Comm (=) f → Comm (=) (intersection_with f).
+  Global Instance difference_with_comm :
+    Comm (=) f → Comm (=) (intersection_with (M:=option A) f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance difference_with_right_id : RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
diff --git a/theories/set.v b/theories/set.v
index 80f060ec..9da42610 100644
--- a/theories/set.v
+++ b/theories/set.v
@@ -24,7 +24,7 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
 Instance set_collection : Collection A (set A).
 Proof. split; [split | |]; by repeat intro. Qed.
 
-Lemma elem_of_top {A} (x : A) : x ∈ ⊤ ↔ True.
+Lemma elem_of_top {A} (x : A) : x ∈ (⊤ : set A) ↔ True.
 Proof. done. Qed.
 Lemma elem_of_mkSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
 Proof. done. Qed.
@@ -40,7 +40,7 @@ Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),
 Instance set_fmap : FMap set := λ A B (f : A → B) (X : set A),
   {[ b | ∃ a, b = f a ∧ a ∈ X ]}.
 Instance set_join : MJoin set := λ A (XX : set (set A)),
-  {[ a | ∃ X, a ∈ X ∧ X ∈ XX ]}.
+  {[ a | ∃ X : set A, a ∈ X ∧ X ∈ XX ]}.
 Instance set_collection_monad : CollectionMonad set.
 Proof. by split; try apply _. Qed.
 
-- 
GitLab