diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 4c2617a7f09960df3b8926fb3318df376b1d8b6e..221ca9b806b725b91727bb981ab7a9d573687ede 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -80,7 +80,7 @@ Proof.
     + iPvsIntro; iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame; eauto. }
       wp_match. by iApply "Hv".
-    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
+    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (@own_valid with "Hγ") as %[].
 Qed.
 End proof.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 841d143d93ffbab854e8b55c522b43bc63640b59..2c169450819a1259c20c058da946a28da790c579 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -103,14 +103,14 @@ Section auth.
     iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
     iInv N as (a') "[Hγ Hφ]".
     iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (own_valid _ with "#Hγ") as "Hvalid".
+    iDestruct (@own_valid with "#Hγ") as "Hvalid".
     iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
     iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
     rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
     { iApply "HΨ"; by iSplit. }
     iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
-    iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
+    iPvs (@own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
     iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
     iNext. iExists (b â‹… af). by iFrame.
   Qed.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index fd10371492499454744d6af34fbdfb640ebd2684..8657892f1f1b3a972641dca84563d60a86023327 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -15,11 +15,11 @@ Section box_defs.
 
   Definition slice_name := gname.
 
-  Definition box_own_auth (γ : slice_name)
-    (a : auth (option (excl bool))) : iProp := own γ (a, ∅).
+  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool)))
+    := own γ (a, (∅:option (agree (later (iPrePropG Λ Σ))))).
 
   Definition box_own_prop (γ : slice_name) (P : iProp) : iProp :=
-    own γ (∅:auth _, Some (to_agree (Next (iProp_unfold P)))).
+    own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
 
   Definition slice_inv (γ : slice_name) (P : iProp) : iProp :=
     (∃ b, box_own_auth γ (● Excl' b) ★ box_own_prop γ P ★ if b then P else True)%I.
@@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
 Proof.
   rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
   iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
-  iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
+  iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
   rewrite -{1}(right_id ∅ _ (Excl' b2)) -{1}(right_id ∅ _ (Excl' b3)).
   by apply auth_update, option_local_update, exclusive_local_update.
 Qed.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index e227bd5ade1f622f7aedd927538dfe060f95ccb3..cd679ccdfbbe142c24487cdc4c060ef39ab91eab 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -18,13 +18,14 @@ Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
 (** * Properties of own *)
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
+Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Λ Σ A _ γ).
 Proof. rewrite !own_eq. solve_proper. Qed.
-Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_proper _.
+Global Instance own_proper γ :
+  Proper ((≡) ==> (⊣⊢)) (@own Λ Σ A _ γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
-Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Λ Σ A _ γ).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
@@ -85,7 +86,7 @@ Section global_empty.
 Context `{i : inG Λ Σ (A:ucmraT)}.
 Implicit Types a : A.
 
-Lemma own_empty γ E : True ={E}=> own γ ∅.
+Lemma own_empty γ E : True ={E}=> own γ (∅:A).
 Proof.
   rewrite ownG_empty !own_eq /own_def.
   apply pvs_ownG_update, iprod_singleton_update_empty.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 6d534c266cdbfe4c294b128aca05a682e9e1db9d..48403855e61fd192d625c7e54af8377c8c4c33c5 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -28,6 +28,7 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
   inG_prf : A = projT2 Σ inG_id (iPreProp Λ (globalF Σ))
 }.
 Arguments inG_id {_ _ _} _.
+Hint Mode inG - - + : typeclass_instances.
 
 Definition to_globalF `{i : inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
   iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
@@ -39,17 +40,18 @@ Section to_globalF.
 Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
-Global Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
+Global Instance to_globalF_ne γ n :
+  Proper (dist n ==> dist n) (@to_globalF Λ Σ A _ γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma to_globalF_op γ a1 a2 :
   to_globalF γ (a1 ⋅ a2) ≡ to_globalF γ a1 ⋅ to_globalF γ a2.
 Proof.
   by rewrite /to_globalF iprod_op_singleton op_singleton cmra_transport_op.
 Qed.
-Global Instance to_globalF_timeless γ m: Timeless m → Timeless (to_globalF γ m).
+Global Instance to_globalF_timeless γ a : Timeless a → Timeless (to_globalF γ a).
 Proof. rewrite /to_globalF; apply _. Qed.
-Global Instance to_globalF_persistent γ m :
-  Persistent m → Persistent (to_globalF γ m).
+Global Instance to_globalF_persistent γ a :
+  Persistent a → Persistent (to_globalF γ a).
 Proof. rewrite /to_globalF; apply _. Qed.
 End to_globalF.
 
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a8180d0e93bc936251dfef5b50a3158fc78a2af6..7152d178f7a8b05edf7b179e188792cac0a67661 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -102,14 +102,14 @@ Section sts.
   Proof.
     iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
     iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ".
-    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (@own_valid with "#Hγ") as %Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
     iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
     iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
     { iApply "HΨ"; by iSplit. }
     iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)".
-    iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+    iPvs (@own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
     iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
     iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
     iNext; iExists s'; by iFrame.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 44b6be39033067723c81cc8dae6a93b89a2109d8..36077d52ee263ed97797971fc0777c21f8f99349 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -5,9 +5,14 @@ From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import invariants.
 Import uPred.
 
+Definition one_shotR (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
+  csumR (exclR unitC) (agreeR $ laterC $ F (iPrePropG Λ Σ)).
+Definition Pending {Λ Σ F} : one_shotR Λ Σ F := Cinl (Excl ()).
+Definition Shot {Λ Σ} {F : cFunctor} (x : F (iPropG Λ Σ)) : one_shotR Λ Σ F :=
+  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
+
 Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
-  one_shot_inG :>
-    inG Λ Σ (csumR (exclR unitC) (agreeR $ laterC $ F (iPrePropG Λ Σ))).
+  one_shot_inG :> inG Λ Σ (one_shotR Λ Σ F).
 Definition oneShotGF (F : cFunctor) : gFunctor :=
   GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))).
 Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
@@ -19,15 +24,13 @@ Definition client eM eW1 eW2 : expr :=
 Global Opaque client.
 
 Section proof.
-Context (G : cFunctor).
-Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}.
+Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ F}.
 Context (N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
-Local Notation X := (G iProp).
+Local Notation X := (F iProp).
 
 Definition barrier_res γ (Φ : X → iProp) : iProp :=
-  (∃ x, own γ (Cinr $ to_agree $
-               Next (cFunctor_map G (iProp_fold, iProp_unfold) x)) ★ Φ x)%I.
+  (∃ x, own γ (Shot x) ★ Φ x)%I.
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp) `{!Closed [] e} :
   recv N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
@@ -57,7 +60,7 @@ Proof.
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
     rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
-    rewrite (ne_proper (cFunctor_map G) (cid, cid) (_ â—Ž _, _ â—Ž _)); last first.
+    rewrite (ne_proper (cFunctor_map F) (cid, cid) (_ â—Ž _, _ â—Ž _)); last first.
     { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
     rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
   iNext. iRewrite -"Hxx" in "Hx'".
@@ -73,7 +76,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
   ⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
 Proof.
   iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
-  iPvs (own_alloc (Cinl (Excl ()))) as (γ) "Hγ". done.
+  iPvs (own_alloc (Pending : one_shotR heap_lang Σ F)) as (γ) "Hγ". done.
   wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
   iFrame "Hh". iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
@@ -81,8 +84,8 @@ Proof.
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
   - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
-    iPvs (own_update _ _ (Cinr (to_agree _)) with "Hγ") as "Hx".
-    by apply cmra_update_exclusive.
+    iPvs (@own_update with "Hγ") as "Hx".
+    { by apply (cmra_update_exclusive (Shot x)). }
     iApply signal_spec; iFrame "Hs"; iSplit; last done.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1539f49e861fae71004d2152eb51f45be76acb42..faaac93142802f4d9b518ff50fa4440cf39bbc83 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -20,22 +20,21 @@ Definition one_shot_example : val := λ: <>,
     end)).
 Global Opaque one_shot_example.
 
-Class one_shotG Σ :=
-  one_shot_inG :> inG heap_lang Σ (csumR (exclR unitC)(dec_agreeR Z)).
-Definition one_shotGF : gFunctorList :=
-  [GFunctor (constRF (csumR (exclR unitC)(dec_agreeR Z)))].
+Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
+Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
+Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR).
+
+Class one_shotG Σ := one_shot_inG :> inG heap_lang Σ one_shotR.
+Definition one_shotGF : gFunctorList := [GFunctor (constRF one_shotR)].
 Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF → one_shotG Σ.
 Proof. intros [? _]; apply: inGF_inG. Qed.
 
-Notation Pending := (Cinl (Excl ())).
-
 Section proof.
 Context `{!heapG Σ, !one_shotG Σ} (N : namespace) (HN : heapN ⊥ N).
 Local Notation iProp := (iPropG heap_lang Σ).
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
-  (l ↦ NONEV ★ own γ Pending ∨
-  ∃ n : Z, l ↦ SOMEV #n ★ own γ (Cinr (DecAgree n)))%I.
+  (l ↦ NONEV ★ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ★ own γ (Shot n))%I.
 
 Lemma wp_one_shot (Φ : val → iProp) :
   heap_ctx ★ (∀ f1 f2 : val,
@@ -52,19 +51,19 @@ Proof.
   - iIntros (n) "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + wp_cas_suc. iSplitL; [|by iLeft].
-      iPvs (own_update with "Hγ") as "Hγ".
-      { by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
+      iPvs (@own_update with "Hγ") as "Hγ".
+      { by apply cmra_update_exclusive with (y:=Shot n). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
     + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
   - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
     iAssert (∃ v, l ↦ v ★ ((v = NONEV ★ own γ Pending) ∨
-       ∃ n : Z, v = SOMEV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
+       ∃ n : Z, v = SOMEV #n ★ own γ (Shot n)))%I with "[-]" as "Hv".
     { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
       + iExists NONEV. iFrame. eauto.
       + iExists (SOMEV #m). iFrame. eauto. }
     iDestruct "Hv" as (v) "[Hl Hv]". wp_load; iPvsIntro.
     iAssert (one_shot_inv γ l ★ (v = NONEV ∨ ∃ n : Z,
-      v = SOMEV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
+      v = SOMEV #n ★ own γ (Shot n)))%I with "[-]" as "[$ #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
@@ -73,10 +72,10 @@ Proof.
     { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]".
-    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (@own_valid with "Hγ") as %?. }
     wp_load; iPvsIntro.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
+    iDestruct (@own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
     wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
 Qed.