diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index b8182aa739eb8fe91e953b5b67822f7738f8f6e1..afe2a07f780188f5854150841890914b9321e5e1 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -7,13 +7,17 @@ Section option.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
+  (* Variant indices. *)
+  Definition none := 0%nat.
+  Definition some := 1%nat.
+
   Definition option_as_mut : val :=
     funrec: <> ["o"] :=
       let: "o'" := !"o" in
       let: "r" := new [ #2 ] in
       case: !"o'" of
-        [ "r" <-{Σ 0} ();; "k" ["r"];
-          "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
+        [ "r" <-{Σ none} ();; "k" ["r"];
+          "r" <-{Σ some} "o'" +ₗ #1;; "k" ["r"] ]
       cont: "k" ["r"] :=
         delete [ #1; "o"];; return: ["r"].
 
@@ -29,9 +33,9 @@ Section option.
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
-      + iApply (type_sum_unit [unit; &uniq{α}τ]%T); [solve_typing..|].
+      + iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
-      + iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|].
+      + iApply (type_sum_assign (option $ &uniq{α}τ)%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
     - iIntros "/= !#". iIntros (k r). inv_vec r=>r. simpl_subst.
       iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 84c34419497ca43632a86ac84e6b120f8941f1ca..0c94b8893bb6a602bd4b652bae3ff2dcc4393aab 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -290,11 +290,11 @@ Section code.
       "rc'" +â‚— #0 <- "count" - #1;;
       if: "count" = #1 then
         (* Return content, delete Rc heap allocation. *)
-        "x" <-{ty.(ty_size),Σ 1} !("rc'" +ₗ #1);;
+        "x" <-{ty.(ty_size),Σ some} !("rc'" +ₗ #1);;
         delete [ #(S ty.(ty_size)); "rc'" ];;
         "k" []
       else
-        "x" <-{Σ 0} ();;
+        "x" <-{Σ none} ();;
         "k" []
       cont: "k" [] :=
         delete [ #1; "rc"];; return: ["x"]).
@@ -384,7 +384,7 @@ Section code.
         iDestruct "Hrc†" as "[Hrc†1 Hrc†2]". iFrame.
         rewrite shift_loc_0. iFrame. iExists [_]. rewrite uninit_own heap_mapsto_vec_singleton.
         auto with iFrame. }
-      iApply (type_sum_memcpy [unit;_]); [solve_typing..|].
+      iApply (type_sum_memcpy (option _)); [solve_typing..|].
       iApply (type_delete (Π[uninit _; uninit _])); [solve_typing..|].
       iApply (type_jump []); solve_typing.
     - iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & _ & Hclose)".
@@ -404,7 +404,7 @@ Section code.
         with "[] LFT Hna HE HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton.
         rewrite !tctx_hasty_val. unlock. iFrame. }
-      iApply (type_sum_unit [unit;ty]); [solve_typing..|].
+      iApply (type_sum_unit (option ty)); [solve_typing..|].
       iApply (type_jump []); solve_typing.
   Qed.
 
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index f046c25d3c77829d71e20bbb0aca93c783da00fc..8fd01e4c92119ce900dec8630eee304e539e3839 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -126,14 +126,14 @@ Section refcell_functions.
       let: "x'" := !"x" in
       let: "n" := !"x'" in
       if: "n" ≤ #-1 then
-        "r" <-{Σ 0} ();;
+        "r" <-{Σ none} ();;
         "k" ["r"] (* FIXME RJ: this is very confusing, "k" does not even look like it is bound here... *)
       else
         "x'" <- "n" + #1;;
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 1} !"ref";;
+        "r" <-{2,Σ some} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       cont: "k" ["r"] :=
@@ -166,7 +166,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_unit [unit; ref α ty]); [solve_typing..|]; first last.
+      iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
@@ -218,7 +218,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_intersect_mono. done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [unit; ref α ty]); [solve_typing..|].
+      iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
@@ -234,11 +234,11 @@ Section refcell_functions.
         let: "ref" := new [ #2 ] in
         "ref" <- "x'" +â‚— #1;;
         "ref" +â‚— #1 <- "x'";;
-        "r" <-{2,Σ 1} !"ref";;
+        "r" <-{2,Σ some} !"ref";;
         delete [ #2; "ref"];;
         "k" ["r"]
       else
-        "r" <-{Σ 0} ();;
+        "r" <-{Σ none} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
         delete [ #1; "x"];; return: ["r"].
@@ -290,7 +290,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [unit; refmut α ty]); [solve_typing..|].
+      iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
@@ -300,7 +300,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_unit [unit; refmut α ty]); [solve_typing..|].
+      iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 1280fc24270a9927be7bdb416e40c83e560edcce..92ae8769f6a9b7d8624913be9894f6c4c18700c6 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -127,11 +127,11 @@ Section rwlock_functions.
        cont: "loop" [] :=
          let: "n" := !ˢᶜ"x'" in
          if: "n" ≤ #-1 then
-           "r" <-{Σ 0} ();;
+           "r" <-{Σ none} ();;
            "k" ["r"]
          else
            if: CAS "x'" "n" ("n" + #1) then
-             "r" <-{Σ 1} "x'";;
+             "r" <-{Σ some} "x'";;
              "k" ["r"]
            else "loop" [])
       cont: "k" ["r"] :=
@@ -171,7 +171,7 @@ Section rwlock_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_unit [unit; rwlockreadguard α ty]);
+      iApply (type_sum_unit (option $ rwlockreadguard α ty));
         [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
@@ -225,7 +225,7 @@ Section rwlock_functions.
           iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
         { rewrite {1}/elctx_interp big_sepL_singleton //. }
-        iApply (type_sum_assign [unit; rwlockreadguard α ty]); [solve_typing..|].
+        iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
         simpl. iApply (type_jump [_]); solve_typing.
       + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
         iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
@@ -244,10 +244,10 @@ Section rwlock_functions.
       let: "r" := new [ #2 ] in
       let: "x'" := !"x" in
       if: CAS "x'" #0 #(-1) then
-        "r" <-{Σ 1} "x'";;
+        "r" <-{Σ some} "x'";;
         "k" ["r"]
       else
-        "r" <-{Σ 0} ();;
+        "r" <-{Σ none} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
         delete [ #1; "x"];; return: ["r"].
@@ -283,7 +283,7 @@ Section rwlock_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_unit [unit; rwlockwriteguard α ty]);
+      iApply (type_sum_unit (option $ rwlockwriteguard α ty));
         [solve_typing..|]; first last.
       rewrite /option /=. iApply (type_jump [_]); solve_typing.
     - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
@@ -298,7 +298,7 @@ Section rwlock_functions.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
       { rewrite {1}/elctx_interp big_sepL_singleton //. }
-      iApply (type_sum_assign [unit; rwlockwriteguard α ty]); [solve_typing..|].
+      iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End rwlock_functions.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 318bb38df21d45f495561d3971e36628d096e6dd..539b0f3775433c4d6b94edfa7c1a2fd69593c9ea 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -167,16 +167,17 @@ Section case.
     iExists i, [_], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
-  Lemma type_sum_assign {E L} tyl i ty1 ty ty1' C T T' p1 p2 e:
+  Lemma type_sum_assign {E L} sty tyl i ty1 ty ty1' C T T' p1 p2 e:
     Closed [] e →
     0 ≤ i →
+    sty = sum tyl →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
     tyl !! (Z.to_nat i) = Some ty →
-    typed_write E L ty1 (sum tyl) ty1' →
+    typed_write E L ty1 sty ty1' →
     typed_body E L C ((p1 ◁ ty1') :: T') e -∗
     typed_body E L C T (p1 <-{Σ i} p2 ;; e).
   Proof.
-    iIntros. rewrite -(Z2Nat.id i) //.
+    iIntros (??->) "* **". rewrite -(Z2Nat.id i) //.
     iApply type_seq; [by eapply type_sum_assign_instr|done|done].
   Qed.
 
@@ -195,16 +196,17 @@ Section case.
     iExists i, [], _. rewrite -Hlen nth_lookup Hty. auto.
   Qed.
 
-  Lemma type_sum_unit {E L} tyl i ty1 ty1' C T T' p e:
+  Lemma type_sum_unit {E L} sty tyl i ty1 ty1' C T T' p e:
     Closed [] e →
     0 ≤ i →
+    sty = sum tyl →
     tctx_extract_hasty E L p ty1 T T' →
     tyl !! (Z.to_nat i) = Some unit →
-    typed_write E L ty1 (sum tyl) ty1' →
+    typed_write E L ty1 sty ty1' →
     typed_body E L C ((p ◁ ty1') :: T') e -∗
     typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
-    iIntros. rewrite -(Z2Nat.id i) //.
+    iIntros (??->) "* **". rewrite -(Z2Nat.id i) //.
     iApply type_seq; [by eapply type_sum_unit_instr|solve_typing|done].
   Qed.
 
@@ -245,18 +247,19 @@ Section case.
     - iExists _. iFrame.
   Qed.
 
-  Lemma type_sum_memcpy {E L} tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
+  Lemma type_sum_memcpy {E L} sty tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
     Closed [] e →
     0 ≤ i →
+    sty = sum tyl →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
     tyl !! (Z.to_nat i) = Some ty →
-    typed_write E L ty1 (sum tyl) ty1' →
+    typed_write E L ty1 sty ty1' →
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
     typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
   Proof.
-    iIntros (????? Hr ?) "?". subst. rewrite -(Z2Nat.id i) //.
+    iIntros (?? -> ??? Hr ?) "?". subst. rewrite -(Z2Nat.id i) //.
     by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
 End case.