add variant of diverging_static for arbitrary invariant lifetime positions

theories/typing/examples/diverging_static.v

@@ -37,4 +37,39 @@ Section diverging_static.
     iIntros "!# *". inv_vec args. simpl_subst.
     iApply type_jump; solve_typing.
   Qed.
+
+  (** Variant of the above where the lifetime is in an arbitrary invariant
+      position.  This is incompatible with branding!
+
+      Our [TyWf] is not working well for type constructors (we have no way of
+      representing the fact that well-formedness is somewhat "uniform"), so we
+      instead work with a constant [Euser] of lifetime inclusion assumptions (in
+      general it could change with the type parameter but only in monotone ways)
+      and a single [κuser] of lifetimes that have to be alive (making κuser a
+      list would require some induction-based reasoning principles that we do
+      not have, but showing that it works for one lifetime is enough to
+      demonstrate the principle). *)
+  Lemma diverging_static_loop_type' (T : lft → type) F κuser Euser call_once
+        `{!TyWf F} :
+    let _ : (∀ κ, TyWf (T κ)) := λ κ, {| ty_lfts := [κ; κuser]; ty_wf_E := Euser |} in
+    (∀ κ1 κ2, (T κ1).(ty_size) = (T κ2).(ty_size)) →
+    (∀ E L κ1 κ2, lctx_lft_eq E L κ1 κ2 → subtype E L (T κ1) (T κ2)) →
+    typed_val call_once (fn(∅; F, T static) → unit) →
+    typed_val (diverging_static_loop call_once)
+              (fn(∀ α, ∅; T α, F) → ∅).
+  Proof.
+    intros HWf HTsz HTsub Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
+    iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
+    { iIntros (k). simpl_subst.
+      iApply type_equivalize_lft_static.
+      iApply (type_call [ϝ] ()); solve_typing. }
+    iIntros "!# *". inv_vec args=>r. simpl_subst.
+    iApply (type_cont [] [] (λ r, [])).
+    { iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
+    iIntros "!# *". inv_vec args. simpl_subst.
+    iApply type_jump; solve_typing.
+  Qed.
+
 End diverging_static.

theories/typing/lft_contexts.v

@@ -332,6 +332,8 @@ Hint Resolve
      elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
   : lrust_typing.
 
+Hint Extern 10 (lctx_lft_eq _ _ _ _) => split : lrust_typing.
+
 Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
 
 Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.

theories/typing/shr_bor.v

@@ -66,8 +66,8 @@ Section typing.
     lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
     subtype E L (&shr{κ1}ty1) (&shr{κ2}ty2).
   Proof. by intros; apply shr_mono. Qed.
-  Lemma shr_proper' E L κ ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (&shr{κ}ty1) (&shr{κ}ty2).
+  Lemma shr_proper' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_eq E L κ1 κ2 → eqtype E L ty1 ty2 → eqtype E L (&shr{κ1}ty1) (&shr{κ2}ty2).
   Proof. by intros; apply shr_proper. Qed.
 
   Lemma tctx_reborrow_shr E L p ty κ κ' :

theories/typing/uniq_bor.v

@@ -104,8 +104,8 @@ Section typing.
     lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
     subtype E L (&uniq{κ1}ty1) (&uniq{κ2}ty2).
   Proof. by intros; apply uniq_mono. Qed.
-  Lemma uniq_proper' E L κ ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (&uniq{κ}ty1) (&uniq{κ}ty2).
+  Lemma uniq_proper' E L κ1 κ2 ty1 ty2 :
+    lctx_lft_eq E L κ1 κ2 → eqtype E L ty1 ty2 → eqtype E L (&uniq{κ1}ty1) (&uniq{κ2}ty2).
   Proof. by intros; apply uniq_proper. Qed.
 
   Lemma tctx_reborrow_uniq E L p ty κ κ' :