From a3d0a33825944449d0f0b129eeb03a1818931708 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 May 2016 02:47:16 +0200
Subject: [PATCH] Tweak the algebraic hierarchy.

- Make the carrier argument of the constructors for the canonical structures
  cofeT and cmraT explicit. This way we make sure the carrier is properly
  exposed, instead of some alias of the carrier.
- Make derived constructions (such as discreteC and discreteR) notations
  instead of definitions. This is yet again to make sure that the carrier is
  properly exposed.
- Turn DRA into a canonical structure (it used to be a type class).

This fixes some issues, notably it fixes some broken rewrites in algebra/sts
and it makes canonical structures work properly with dec_agree.
---
 algebra/agree.v           |   5 +-
 algebra/auth.v            |   5 +-
 algebra/cmra.v            |  50 ++++++-----
 algebra/cofe.v            |  25 +++---
 algebra/cofe_solver.v     |   2 +-
 algebra/dec_agree.v       |   5 +-
 algebra/dra.v             | 185 +++++++++++++++++++++++++-------------
 algebra/excl.v            |   5 +-
 algebra/frac.v            |   5 +-
 algebra/gmap.v            |   5 +-
 algebra/iprod.v           |   5 +-
 algebra/list.v            |   5 +-
 algebra/one_shot.v        |   5 +-
 algebra/option.v          |   5 +-
 algebra/sts.v             |  75 +++++++---------
 algebra/upred.v           |   2 +-
 program_logic/resources.v |   5 +-
 tests/one_shot.v          |   3 +-
 18 files changed, 233 insertions(+), 164 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index cb82e126c..ecc0bd975 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -49,7 +49,7 @@ Proof.
   - intros n c; apply and_wlog_r; intros;
       symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
-Canonical Structure agreeC := CofeT agree_cofe_mixin.
+Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
 
 Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n.
 Proof. by intros [??] Hxy; apply Hxy. Qed.
@@ -116,7 +116,8 @@ Proof.
     + by rewrite agree_idemp.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
-Canonical Structure agreeR : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
+Canonical Structure agreeR : cmraT :=
+  CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
 
 Global Instance agree_persistent (x : agree A) : Persistent x.
 Proof. done. Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 5a103b231..a1ffd49f3 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -51,7 +51,7 @@ Proof.
   - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
     apply (conv_compl n (chain_map own c)).
 Qed.
-Canonical Structure authC := CofeT auth_cofe_mixin.
+Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
 
 Global Instance Auth_timeless a b :
   Timeless a → Timeless b → Timeless (Auth a b).
@@ -128,7 +128,8 @@ Proof.
       as (b&?&?&?); auto using own_validN.
     by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
 Qed.
-Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
+Canonical Structure authR : cmraT :=
+  CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
   split; first apply _.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index fadeb8576..e9cc36887 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -62,7 +62,7 @@ Structure cmraT := CMRAT {
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car
 }.
-Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
+Arguments CMRAT _ {_ _ _ _ _ _ _} _ _.
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
@@ -75,7 +75,7 @@ Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
 Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
-Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
+Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
 (** Lifting properties from the mixin *)
@@ -474,14 +474,14 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Class RA A `{Equiv A, Core A, Op A, Valid A} := {
+Record RAMixin A `{Equiv A, Core A, Op A, Valid A} := {
   (* setoids *)
   ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
-  ra_core_ne :> Proper ((≡) ==> (≡)) core;
-  ra_validN_ne :> Proper ((≡) ==> impl) valid;
+  ra_core_ne : Proper ((≡) ==> (≡)) core;
+  ra_validN_ne : Proper ((≡) ==> impl) valid;
   (* monoid *)
-  ra_assoc :> Assoc (≡) (⋅);
-  ra_comm :> Comm (≡) (⋅);
+  ra_assoc : Assoc (≡) (⋅);
+  ra_comm : Comm (≡) (⋅);
   ra_core_l x : core x ⋅ x ≡ x;
   ra_core_idemp x : core (core x) ≡ core x;
   ra_core_preserving x y : x ≼ y → core x ≼ core y;
@@ -489,36 +489,41 @@ Class RA A `{Equiv A, Core A, Op A, Valid A} := {
 }.
 
 Section discrete.
-  Context {A : cofeT} `{Discrete A}.
-  Context `{Core A, Op A, Valid A} (ra : RA A).
+  Context `{Equiv A, Core A, Op A, Valid A, @Equivalence A (≡)}.
+  Context (ra_mix : RAMixin A).
+  Existing Instances discrete_dist discrete_compl.
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
-    destruct ra; split; unfold Proper, respectful, includedN;
-      try setoid_rewrite <-(timeless_iff _ _); try done.
+    destruct ra_mix; split; try done.
     - intros x; split; first done. by move=> /(_ 0).
-    - intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
-      apply (timeless _), dist_le with n; auto with lia.
+    - intros n x y1 y2 ??; by exists (y1,y2).
   Qed.
-  Definition discreteR : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
-  Global Instance discrete_cmra_discrete : CMRADiscrete discreteR.
-  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
 End discrete.
 
+Notation discreteR A ra_mix :=
+  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
+Notation discreteLeibnizR A ra_mix :=
+  (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
+
+Global Instance discrete_cmra_discrete `{Equiv A, Core A, Op A, Valid A,
+  @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
+Proof. split. apply _. done. Qed.
+
 (** ** CMRA for the unit type *)
 Section unit.
   Instance unit_valid : Valid () := λ x, True.
+  Instance unit_validN : ValidN () := λ n x, True.
   Instance unit_core : Core () := λ x, x.
   Instance unit_op : Op () := λ x y, ().
   Global Instance unit_empty : Empty () := ().
-  Definition unit_ra : RA ().
-  Proof. by split. Qed.
-  Canonical Structure unitR : cmraT :=
-    Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
+  Definition unit_cmra_mixin : CMRAMixin ().
+  Proof. by split; last exists ((),()). Qed.
+  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
   Global Instance unit_cmra_unit : CMRAUnit unitR.
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
-  Proof. by apply discrete_cmra_discrete. Qed.
+  Proof. done. Qed.
   Global Instance unit_persistent (x : ()) : Persistent x.
   Proof. done. Qed.
 End unit.
@@ -563,7 +568,8 @@ Section prod.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
       by exists ((z1.1,z2.1),(z1.2,z2.2)).
   Qed.
-  Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
+  Canonical Structure prodR : cmraT :=
+    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
   Global Instance prod_cmra_unit `{Empty A, Empty B} :
     CMRAUnit A → CMRAUnit B → CMRAUnit prodR.
   Proof.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 301e03996..c3cefe2fd 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -65,7 +65,7 @@ Structure cofeT := CofeT {
   cofe_compl : Compl cofe_car;
   cofe_mixin : CofeMixin cofe_car
 }.
-Arguments CofeT {_ _ _ _} _.
+Arguments CofeT _ {_ _ _} _.
 Add Printing Constructor cofeT.
 Existing Instances cofe_equiv cofe_dist cofe_compl.
 Arguments cofe_car : simpl never.
@@ -239,7 +239,7 @@ Section cofe_mor.
     - intros n c x; simpl.
       by rewrite (conv_compl n (fun_chain c x)) /=.
   Qed.
-  Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
+  Canonical Structure cofe_mor : cofeT := CofeT (cofeMor A B) cofe_mor_cofe_mixin.
 
   Global Instance cofe_mor_car_ne n :
     Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
@@ -291,7 +291,7 @@ Section unit.
   Instance unit_compl : Compl unit := λ _, ().
   Definition unit_cofe_mixin : CofeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
-  Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
+  Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
   Global Instance unit_discrete_cofe : Discrete unitC.
   Proof. done. Qed.
 End unit.
@@ -317,7 +317,7 @@ Section product.
     - intros n c; split. apply (conv_compl n (chain_map fst c)).
       apply (conv_compl n (chain_map snd c)).
   Qed.
-  Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
+  Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
   Global Instance pair_timeless (x : A) (y : B) :
     Timeless x → Timeless y → Timeless (x,y).
   Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
@@ -436,15 +436,16 @@ Section discrete_cofe.
     - intros n c. rewrite /compl /discrete_compl /=;
       symmetry; apply (chain_cauchy c 0 n). omega.
   Qed.
-  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
-  Global Instance discrete_discrete_cofe : Discrete discreteC.
-  Proof. by intros x y. Qed.
 End discrete_cofe.
-Arguments discreteC _ {_ _}.
 
-Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
-Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
-Proof. by intros A x y. Qed.
+Notation discreteC A := (CofeT A discrete_cofe_mixin).
+Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).
+
+Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} :
+  Discrete (discreteC A).
+Proof. by intros x y. Qed.
+Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
+Proof. by intros x y. Qed.
 
 Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
@@ -478,7 +479,7 @@ Section later.
     - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
     - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
   Qed.
-  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
+  Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
   Global Instance Next_contractive : Contractive (@Next A).
   Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 280dce025..515028163 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -71,7 +71,7 @@ Proof.
   - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
     apply (chain_cauchy c); lia.
 Qed.
-Definition T : cofeT := CofeT tower_cofe_mixin.
+Definition T : cofeT := CofeT tower tower_cofe_mixin.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
   match i with 0 => cid | S i => f (i + k) â—Ž ff i end.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 2eeaeaa51..07352633a 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -28,7 +28,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
   end.
 Instance dec_agree_core : Core (dec_agree A) := id.
 
-Definition dec_agree_ra : RA (dec_agree A).
+Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
 Proof.
   split.
   - apply _.
@@ -42,7 +42,8 @@ Proof.
   - by intros [?|] [?|] ?.
 Qed.
 
-Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
+Canonical Structure dec_agreeR : cmraT :=
+  discreteR (dec_agree A) dec_agree_ra_mixin.
 
 (* Some properties of this CMRA *)
 Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
diff --git a/algebra/dra.v b/algebra/dra.v
index b2a0439d0..6d2e9c893 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -1,53 +1,112 @@
 From iris.algebra Require Export cmra.
 
-(** From disjoint pcm *)
-Record validity {A} (P : A → Prop) : Type := Validity {
-  validity_car : A;
-  validity_is_valid : Prop;
-  validity_prf : validity_is_valid → P validity_car
-}.
-Add Printing Constructor validity.
-Arguments Validity {_ _} _ _ _.
-Arguments validity_car {_ _} _.
-Arguments validity_is_valid {_ _} _.
-
-Definition to_validity {A} {P : A → Prop} (x : A) : validity P :=
-  Validity x (P x) id.
-
-Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A} := {
+Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
-  dra_equivalence :> Equivalence ((≡) : relation A);
-  dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  dra_core_proper :> Proper ((≡) ==> (≡)) core;
-  dra_valid_proper :> Proper ((≡) ==> impl) valid;
-  dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
+  mixin_dra_equivalence : Equivalence ((≡) : relation A);
+  mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
+  mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
+  mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
+  mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
   (* validity *)
-  dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  dra_core_valid x : ✓ x → ✓ core x;
+  mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
+  mixin_dra_core_valid x : ✓ x → ✓ core x;
   (* monoid *)
-  dra_assoc :> Assoc (≡) (⋅);
-  dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
-  dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
-  dra_symmetric :> Symmetric (@disjoint A _);
-  dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  dra_core_disjoint_l x : ✓ x → core x ⊥ x;
-  dra_core_l x : ✓ x → core x ⋅ x ≡ x;
-  dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  dra_core_preserving x y : 
+  mixin_dra_assoc : Assoc (≡) (⋅);
+  mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
+  mixin_dra_disjoint_move_l x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
+  mixin_dra_symmetric : Symmetric (@disjoint A _);
+  mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
+  mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
+  mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
+  mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
+  mixin_dra_core_preserving x y : 
     ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
 }.
+Structure draT := DRAT {
+  dra_car :> Type;
+  dra_equiv : Equiv dra_car;
+  dra_core : Core dra_car;
+  dra_disjoint : Disjoint dra_car;
+  dra_op : Op dra_car;
+  dra_valid : Valid dra_car;
+  dra_mixin : DRAMixin dra_car
+}.
+Arguments DRAT _ {_ _ _ _ _} _.
+Arguments dra_car : simpl never.
+Arguments dra_equiv : simpl never.
+Arguments dra_core : simpl never.
+Arguments dra_disjoint : simpl never.
+Arguments dra_op : simpl never.
+Arguments dra_valid : simpl never.
+Arguments dra_mixin : simpl never.
+Add Printing Constructor draT.
+Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
 
+(** Lifting properties from the mixin *)
+Section dra_mixin.
+  Context {A : draT}.
+  Implicit Types x y : A.
+  Global Instance dra_equivalence : Equivalence ((≡) : relation A).
+  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
+  Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
+  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
+  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
+  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
+  Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
+  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
+  Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
+  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
+  Lemma dra_core_valid x : ✓ x → ✓ core x.
+  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
+  Global Instance dra_assoc : Assoc (≡) (@op A _).
+  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
+  Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
+  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
+  Lemma dra_disjoint_move_l x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
+  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
+  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
+  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
+  Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
+  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
+  Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
+  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
+  Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
+  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
+  Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
+  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
+  Lemma dra_core_preserving x y : 
+    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
+  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
+End dra_mixin.
+
+Record validity (A : draT) := Validity {
+  validity_car : A;
+  validity_is_valid : Prop;
+  validity_prf : validity_is_valid → valid validity_car
+}.
+Add Printing Constructor validity.
+Arguments Validity {_} _ _ _.
+Arguments validity_car {_} _.
+Arguments validity_is_valid {_} _.
+
+Definition to_validity {A : draT} (x : A) : validity A :=
+  Validity x (valid x) id.
+
+(* The actual construction *)
 Section dra.
-Context A `{DRA A}.
+Context (A : draT).
+Implicit Types a b : A.
+Implicit Types x y z : validity A.
 Arguments valid _ _ !_ /.
-Hint Immediate dra_op_proper : typeclass_instances.
-
-Notation T := (validity (valid : A → Prop)).
 
-Instance validity_valid : Valid T := validity_is_valid.
-Instance validity_equiv : Equiv T := λ x y,
+Instance validity_valid : Valid (validity A) := validity_is_valid.
+Instance validity_equiv : Equiv (validity A) := λ x y,
   (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence ((≡) : relation T).
+Instance validity_equivalence : Equivalence (@equiv (validity A) _).
 Proof.
   split; unfold equiv, validity_equiv.
   - by intros [x px ?]; simpl.
@@ -55,40 +114,43 @@ Proof.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; trans y]; tauto.
 Qed.
+Canonical Structure validityC : cofeT := discreteC (validity A).
+
 Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply dra_valid_proper. Qed.
-Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
+Proof. by split; apply: dra_valid_proper. Qed.
+Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
 Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
+Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
 Proof.
   intros x1 x2 Hx y1 y2 Hy; split.
   - by rewrite Hy (symmetry_iff (⊥) x1) (symmetry_iff (⊥) x2) Hx.
   - by rewrite -Hy (symmetry_iff (⊥) x2) (symmetry_iff (⊥) x1) -Hx.
 Qed.
-Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
-Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
+
+Lemma dra_disjoint_rl a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
+Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
+Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
 Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r x y z :
-  ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
+Lemma dra_disjoint_move_r a b c :
+  ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
 Proof.
   intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
   apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
 Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
 
-Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
+Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
 Hint Resolve validity_valid_car_valid.
-Program Instance validity_core : Core T := λ x,
+Program Instance validity_core : Core (validity A) := λ x,
   Validity (core (validity_car x)) (✓ x) _.
-Solve Obligations with naive_solver auto using dra_core_valid.
-Program Instance validity_op : Op T := λ x y,
+Solve Obligations with naive_solver eauto using dra_core_valid.
+Program Instance validity_op : Op (validity A) := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
-Solve Obligations with naive_solver auto using dra_op_valid.
+Solve Obligations with naive_solver eauto using dra_op_valid.
 
-Definition validity_ra : RA (discreteC T).
+Definition validity_ra_mixin : RAMixin (validity A).
 Proof.
   split.
   - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
@@ -98,7 +160,7 @@ Proof.
   - intros ?? [??]; naive_solver.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
       [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |by intros; rewrite assoc].
+      |intros; by rewrite assoc].
   - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
   - intros [x px ?]; split;
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
@@ -111,21 +173,20 @@ Proof.
     + intros. rewrite Hy //. tauto.
   - by intros [x px ?] [y py ?] (?&?&?).
 Qed.
-Definition validityR : cmraT := discreteR validity_ra.
-Instance validity_cmra_discrete :
-  CMRADiscrete validityR := discrete_cmra_discrete _.
+Canonical Structure validityR : cmraT :=
+  discreteR (validity A) validity_ra_mixin.
 
-Lemma validity_update (x y : validityR) :
-  (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
+Lemma validity_update x y :
+  (∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
 Proof.
   intros Hxy; apply cmra_discrete_update=> z [?[??]].
   split_and!; try eapply Hxy; eauto.
 Qed.
 
-Lemma to_validity_op (x y : A) :
-  (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) →
-  to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
-Proof. split; naive_solver auto using dra_op_valid. Qed.
+Lemma to_validity_op a b :
+  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
+  to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
+Proof. split; naive_solver eauto using dra_op_valid. Qed.
 
 (* TODO: This has to be proven again. *)
 (*
diff --git a/algebra/excl.v b/algebra/excl.v
index bca3134c9..356f06d84 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -59,7 +59,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
+Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
 Global Instance excl_discrete : Discrete A → Discrete exclC.
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
@@ -107,7 +107,8 @@ Proof.
       | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
       end; destruct y1, y2; inversion_clear Hx; repeat constructor.
 Qed.
-Canonical Structure exclR : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
+Canonical Structure exclR : cmraT :=
+  CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
 Global Instance excl_cmra_unit : CMRAUnit exclR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
diff --git a/algebra/frac.v b/algebra/frac.v
index f1ec2c20e..ede01ba39 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -72,7 +72,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first lia;
        constructor; destruct (c 0); simplify_eq/=.
 Qed.
-Canonical Structure fracC : cofeT := CofeT frac_cofe_mixin.
+Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin.
 Global Instance frac_discrete : Discrete A → Discrete fracC.
 Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
 Global Instance frac_leibniz : LeibnizEquiv A → LeibnizEquiv (frac A).
@@ -157,7 +157,8 @@ Proof.
     + exists (∅, Frac q a); inversion_clear Hx'; by repeat constructor.
     + exfalso; inversion_clear Hx'.
 Qed.
-Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
+Canonical Structure fracR : cmraT :=
+  CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin.
 Global Instance frac_cmra_unit : CMRAUnit fracR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index e85f39dd7..30d2f51aa 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -28,7 +28,7 @@ Proof.
     feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
     by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
-Canonical Structure gmapC : cofeT := CofeT gmap_cofe_mixin.
+Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
 Global Instance gmap_discrete : Discrete A → Discrete gmapC.
 Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 (* why doesn't this go automatic? *)
@@ -152,7 +152,8 @@ Proof.
       pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
       by symmetry; apply option_op_positive_dist_r with (m1 !! i).
 Qed.
-Canonical Structure gmapR : cmraT := CMRAT gmap_cofe_mixin gmap_cmra_mixin.
+Canonical Structure gmapR : cmraT :=
+  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
 Global Instance gmap_cmra_unit : CMRAUnit gmapR.
 Proof.
   split.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index b9dd41fad..3a3883e93 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -42,7 +42,7 @@ Section iprod_cofe.
       rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
       apply (chain_cauchy c); lia.
   Qed.
-  Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
+  Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
 
   (** Properties of empty *)
   Section empty.
@@ -153,7 +153,8 @@ Section iprod_cmra.
       exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
       split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
-  Canonical Structure iprodR : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
+  Canonical Structure iprodR : cmraT :=
+    CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
   Global Instance iprod_cmra_unit `{∀ x, Empty (B x)} :
     (∀ x, CMRAUnit (B x)) → CMRAUnit iprodR.
   Proof.
diff --git a/algebra/list.v b/algebra/list.v
index 058f2803e..581ba0665 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -68,7 +68,7 @@ Proof.
     rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
     by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
 Qed.
-Canonical Structure listC := CofeT list_cofe_mixin.
+Canonical Structure listC := CofeT (list A) list_cofe_mixin.
 Global Instance list_discrete : Discrete A → Discrete listC.
 Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
 
@@ -196,7 +196,8 @@ Section cmra.
           [inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
         exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
   Qed.
-  Canonical Structure listR : cmraT := CMRAT list_cofe_mixin list_cmra_mixin.
+  Canonical Structure listR : cmraT :=
+    CMRAT (list A) list_cofe_mixin list_cmra_mixin.
 
   Global Instance empty_list : Empty (list A) := [].
   Global Instance list_cmra_unit : CMRAUnit listR.
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 18db970bb..72588fd9c 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -65,7 +65,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin.
+Canonical Structure one_shotC : cofeT := CofeT (one_shot A) one_shot_cofe_mixin.
 Global Instance one_shot_discrete : Discrete A → Discrete one_shotC.
 Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed.
 Global Instance one_shot_leibniz : LeibnizEquiv A → LeibnizEquiv (one_shot A).
@@ -186,7 +186,8 @@ Proof.
        * exists (Shot a, ∅). inversion_clear Hx'. by repeat constructor.
        * exists (∅, Shot a). inversion_clear Hx'. by repeat constructor.
 Qed.
-Canonical Structure one_shotR : cmraT := CMRAT one_shot_cofe_mixin one_shot_cmra_mixin.
+Canonical Structure one_shotR : cmraT :=
+  CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin.
 Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR.
diff --git a/algebra/option.v b/algebra/option.v
index 86007543a..c7e4b1bd8 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -34,7 +34,7 @@ Proof.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure optionC := CofeT option_cofe_mixin.
+Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
 Global Instance option_discrete : Discrete A → Discrete optionC.
 Proof. destruct 2; constructor; by apply (timeless _). Qed.
 
@@ -110,7 +110,8 @@ Proof.
     + by exists (None,Some x); inversion Hx'; repeat constructor.
     + exists (None,None); repeat constructor.
 Qed.
-Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin.
+Canonical Structure optionR :=
+  CMRAT (option A) option_cofe_mixin option_cmra_mixin.
 Global Instance option_cmra_unit : CMRAUnit optionR.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
diff --git a/algebra/sts.v b/algebra/sts.v
index 156becc0b..7950bf8cd 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -155,15 +155,6 @@ Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed.
 End sts.
 
 Notation steps := (rtc step).
-End sts.
-
-Notation stsT := sts.stsT.
-Notation STS := sts.STS.
-
-(** * STSs form a disjoint RA *)
-(* This module should never be imported, uses the module [sts] below. *)
-Module sts_dra.
-Import sts.
 
 (* The type of bounds we can give to the state of an STS. This is the type
    that we equip with an RA structure. *)
@@ -172,22 +163,28 @@ Inductive car (sts : stsT) :=
   | frag : set (state sts) → set (token sts ) → car sts.
 Arguments auth {_} _ _.
 Arguments frag {_} _ _.
+End sts.
 
+Notation stsT := sts.stsT.
+Notation STS := sts.STS.
+
+(** * STSs form a disjoint RA *)
 Section sts_dra.
-Context {sts : stsT}.
+Context (sts : stsT).
+Import sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
 
 Inductive sts_equiv : Equiv (car sts) :=
   | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
-Global Existing Instance sts_equiv.
-Global Instance sts_valid : Valid (car sts) := λ x,
+Existing Instance sts_equiv.
+Instance sts_valid : Valid (car sts) := λ x,
   match x with
   | auth s T => tok s ⊥ T
   | frag S' T => closed S' T ∧ S' ≢ ∅
   end.
-Global Instance sts_core : Core (car sts) := λ x,
+Instance sts_core : Core (car sts) := λ x,
   match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
@@ -197,8 +194,8 @@ Inductive sts_disjoint : Disjoint (car sts) :=
      S1 ∩ S2 ≢ ∅ → T1 ⊥ T2 → frag S1 T1 ⊥ frag S2 T2
   | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → auth s T1 ⊥ frag S T2
   | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → frag S T1 ⊥ auth s T2.
-Global Existing Instance sts_disjoint.
-Global Instance sts_op : Op (car sts) := λ x1 x2,
+Existing Instance sts_disjoint.
+Instance sts_op : Op (car sts) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
@@ -212,14 +209,19 @@ Hint Extern 50 (_ ∈ _) => set_solver : sts.
 Hint Extern 50 (_ ⊆ _) => set_solver : sts.
 Hint Extern 50 (_ ⊥ _) => set_solver : sts.
 
-Global Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
+Global Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s).
+Proof. by constructor. Qed.
+Global Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts).
+Proof. by constructor. Qed.
+
+Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
 Proof.
   split.
   - by intros []; constructor.
   - by destruct 1; constructor.
   - destruct 1; inversion_clear 1; constructor; etrans; eauto.
 Qed.
-Global Instance sts_dra : DRA (car sts).
+Lemma sts_dra_mixin : DRAMixin (car sts).
 Proof.
   split.
   - apply _.
@@ -254,19 +256,20 @@ Proof.
            unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
         end; auto with sts.
 Qed.
-Canonical Structure R : cmraT := validityR (car sts).
-End sts_dra. End sts_dra.
+Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
+End sts_dra.
 
 (** * The STS Resource Algebra *)
 (** Finally, the general theory of STS that should be used by users *)
-Notation stsR := (@sts_dra.R).
+Notation stsC sts := (validityC (stsDR sts)).
+Notation stsR sts := (validityR (stsDR sts)).
 
 Section sts_definitions.
   Context {sts : stsT}.
   Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
-    to_validity (sts_dra.auth s T).
+    to_validity (sts.auth s T).
   Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
-    to_validity (sts_dra.frag S T).
+    to_validity (sts.frag S T).
   Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
     sts_frag (sts.up s T) T.
 End sts_definitions.
@@ -280,23 +283,15 @@ Context {sts : stsT}.
 Implicit Types s : state sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
-
-Global Instance sts_cmra_discrete : CMRADiscrete (stsR sts).
-Proof. apply validity_cmra_discrete. Qed.
+Arguments dra_valid _ !_/.
 
 (** Setoids *)
 Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
-Proof. (* this proof is horrible *)
-  intros T1 T2 HT. rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
+Proof. solve_proper. Qed.
 Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
-Proof.
-  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
+Proof. solve_proper. Qed.
 Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
-Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
+Proof. solve_proper. Qed.
 
 (** Validity *)
 Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ⊥ T.
@@ -334,11 +329,8 @@ Lemma sts_op_frag S1 S2 T1 T2 :
   T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
-  intros HT HS1 HS2. rewrite /sts_frag.
-  (* FIXME why does rewrite not work?? *)
-  etrans; last eapply to_validity_op; first done; [].
-  move=>/=[??]. split_and!; [auto; set_solver..|].
-  constructor; done.
+  intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
+  move=>/=[??]. split_and!; [auto; set_solver..|by constructor].
 Qed.
 
 (** Frame preserving updates *)
@@ -367,9 +359,8 @@ Proof.
   rewrite <-HT. eapply up_subseteq; done.
 Qed.
 
-Lemma up_set_intersection S1 Sf Tf :
-  closed Sf Tf → 
-  S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
+Lemma sts_up_set_intersection S1 Sf Tf :
+  closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
 Proof.
   intros Hclf. apply (anti_symm (⊆)).
   + move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
diff --git a/algebra/upred.v b/algebra/upred.v
index 2a974d2be..0e31b28cf 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -47,7 +47,7 @@ Section cofe.
     - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
     - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
   Qed.
-  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
+  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
 End cofe.
 Arguments uPredC : clear implicits.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 7d7714521..c07686035 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -66,7 +66,7 @@ Proof.
     + apply (conv_compl n (chain_map pst c)).
     + apply (conv_compl n (chain_map gst c)).
 Qed.
-Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
+Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
 Global Instance res_timeless r :
   Timeless (wld r) → Timeless (gst r) → Timeless r.
 Proof. by destruct 3; constructor; try apply: timeless. Qed.
@@ -118,7 +118,8 @@ Proof.
       (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
     by exists (Res w σ m, Res w' σ' m').
 Qed.
-Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
+Canonical Structure resR : cmraT :=
+  CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
 Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
 Proof.
   split.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 8ca7e243b..22fe7d867 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,8 +52,7 @@ Proof.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
     + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
       iPvs (own_update with "Hγ") as "Hγ".
-      { (* FIXME: canonical structures are not working *)
-        by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
+      { by apply (one_shot_update_shoot (DecAgree n)). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
     + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
-- 
GitLab