also prove faking a shared uniq ref

_CoqProject

@@ -53,7 +53,7 @@ theories/typing/typing.v
 theories/typing/soundness.v
 theories/typing/lib/panic.v
 theories/typing/lib/option.v
-theories/typing/lib/fake_shared_box.v
+theories/typing/lib/fake_shared.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/join.v

theories/typing/lib/fake_shared_box.v → theories/typing/lib/fake_shared.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
-Section fake_shared_box.
+Section fake_shared.
   Context `{typeG Σ}.
 
   Definition fake_shared_box : val :=
@@ -25,7 +25,7 @@ Section fake_shared_box.
       { iApply frac_bor_iff; last done. iIntros "!>!# *".
         rewrite heap_mapsto_vec_singleton. iSplit; auto. }
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
-      by iApply ty_shr_mono. }
+      simpl. by iApply ty_shr_mono. }
     do 2 wp_seq.
     iApply (type_type [] _ _ [ x ◁ box (&shr{α}(box ty)) ]
             with "[] LFT [] Hna HL Hk [HT]"); last first.
@@ -33,4 +33,34 @@ Section fake_shared_box.
     { by rewrite /elctx_interp. }
     iApply type_jump; simpl; solve_typing.
   Qed.
-End fake_shared_box.
+
+  Definition fake_shared_uniq : val :=
+    funrec: <> ["x"] := Skip ;; return: ["x"].
+
+  Lemma fake_shared_uniq_type ty `{!TyWf ty} :
+    typed_val fake_shared_box
+      (fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(&uniq{β} ty)).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
+    rewrite tctx_interp_singleton tctx_hasty_val.
+    iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
+    (* FIXME: WTF, using &uniq{β} here does not work. *)
+    iAssert (▷ ty_own (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
+    { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
+      iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
+      iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
+      iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
+      { iApply frac_bor_iff; last done. iIntros "!>!# *".
+        rewrite heap_mapsto_vec_singleton. iSplit; auto. }
+      iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+      simpl. iApply ty_shr_mono; last done. iApply lft_intersect_incl_l. }
+    do 2 wp_seq.
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}(&uniq{β} ty)) ]
+            with "[] LFT [] Hna HL Hk [HT]"); last first.
+    { by rewrite tctx_interp_singleton tctx_hasty_val. }
+    { by rewrite /elctx_interp. }
+    iApply type_jump; simpl; solve_typing.
+  Qed.
+End fake_shared.