Make type class inference for inG less eager.

This way, it won't pick arbitrary (and possibly wrong!) inG instances
when multiple ones are available. We achieve this by declaring:

  Hint Mode inG - - +

So that type class inference only succeeds when the type of the ghost
variable does not include any evars.

This required me to make some minor changes throughout the whole
development making some types explicit.

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.
 

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.

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.

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.

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.
 

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.

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.

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.