Adapt to coq/coq#8829 (Error when [foo.(bar)] is used with nonprojection [bar])

theories/typing/function.v

@@ -10,8 +10,8 @@ Section fn.
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
   Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
-    FP (λ ϝ, E ϝ ++ tys.(tyl_wf_E) ++ tys.(tyl_outlives_E) ϝ ++
-                    ty.(ty_wf_E) ++ ty.(ty_outlives_E) ϝ)
+    FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
+                    ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
        tys ty.
 
   (* The other alternative for defining the fn type would be to state

theories/typing/lib/diverging_static.v

@@ -22,7 +22,7 @@ Section diverging_static.
     (* F : FnOnce(&'static T), as witnessed by the impl call_once *)
     typed_val call_once (fn(∅; F, &shr{static} T) → unit) →
     typed_val (diverging_static_loop call_once)
-              (fn(∀ α, λ ϝ, T.(ty_outlives_E) static; &shr{α} T, F) → ∅).
+              (fn(∀ α, λ ϝ, ty_outlives_E T static; &shr{α} T, F) → ∅).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.

theories/typing/lib/mutex/mutexguard.v

@@ -74,7 +74,7 @@ Section mguard.
   Qed.
 
   Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance mutexguard_type_contractive α : TypeContractive (mutexguard α).
   Proof.

theories/typing/lib/refcell/ref.v

@@ -70,7 +70,7 @@ Section ref.
   Qed.
 
   Global Instance ref_wf α ty `{!TyWf ty} : TyWf (ref α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance ref_type_contractive α : TypeContractive (ref α).
   Proof. solve_type_proper. Qed.

theories/typing/lib/refcell/refmut.v

@@ -75,7 +75,7 @@ Section refmut.
   Qed.
 
   Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance refmut_type_contractive α : TypeContractive (refmut α).
   Proof. solve_type_proper. Qed.

theories/typing/lib/rwlock/rwlockreadguard.v

@@ -62,7 +62,7 @@ Section rwlockreadguard.
   Qed.
 
   Global Instance rwlockreadguard_wf α ty `{!TyWf ty} : TyWf (rwlockreadguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance rwlockreadguard_type_contractive α : TypeContractive (rwlockreadguard α).
   Proof.

theories/typing/lib/rwlock/rwlockwriteguard.v

@@ -62,7 +62,7 @@ Section rwlockwriteguard.
   Qed.
 
   Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
-    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) α }.
+    { ty_lfts := [α]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty α }.
 
   Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
   Proof.

theories/typing/lib/spawn.v

@@ -79,7 +79,7 @@ Section spawn.
   Lemma spawn_type fty retty call_once `{!TyWf fty, !TyWf retty}
         `(!Send fty, !Send retty) :
     typed_val call_once (fn(∅; fty) → retty) → (* fty : FnOnce() -> retty, as witnessed by the impl call_once *)
-    let E ϝ := fty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
+    let E ϝ := ty_outlives_E fty static ++ ty_outlives_E retty static in
     typed_val (spawn call_once) (fn(E; fty) → join_handle retty).
   Proof.
     intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".

theories/typing/product.v

@@ -157,7 +157,7 @@ Section product.
   Definition unit := product [].
 
   Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
-    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+    { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Lemma outlives_product ty1 ty2 ϝ `{!TyWf ty1, !TyWf ty2} :
     ty_outlives_E (product [ty1; ty2]) ϝ = ty_outlives_E ty1 ϝ ++ ty_outlives_E ty2 ϝ.

theories/typing/shr_bor.v

@@ -16,7 +16,7 @@ Section shr_bor.
   Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
 
   Global Instance shr_bor_wf κ ty `{!TyWf ty} : TyWf (shr_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
 
   Lemma shr_type_incl κ1 κ2 ty1 ty2 :
     κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).

theories/typing/sum.v

@@ -84,7 +84,7 @@ Section sum.
   Qed.
 
   Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
-    { ty_lfts := tyl.(tyl_lfts); ty_wf_E := tyl.(tyl_wf_E) }.
+    { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
   Proof.

theories/typing/type.v

@@ -60,9 +60,9 @@ Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
 Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
-  ty.(ty_outlives_E) β ⊆+ E →
+  ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
-  elctx_sat E L (ty.(ty_outlives_E) α).
+  elctx_sat E L (ty_outlives_E ty α).
 Proof.
   unfold ty_outlives_E. induction ty.(ty_lfts) as [|κ l IH]=>/= Hsub Hαβ.
   - solve_typing.
@@ -96,14 +96,14 @@ Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
 Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_outlives_E) κ
-  | tyl_wf_cons ty tyl => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
+  | tyl_wf_cons ty [] => ty_outlives_E ty κ
+  | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
 Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
-  tyl.(tyl_outlives_E) β ⊆+ E →
+  tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
-  elctx_sat E L (tyl.(tyl_outlives_E) α).
+  elctx_sat E L (tyl_outlives_E tyl α).
 Proof.
   induction WF as [|? [] ?? IH]=>/=.
   - solve_typing.

theories/typing/uniq_bor.v

@@ -42,7 +42,7 @@ Section uniq_bor.
   Qed.
 
   Global Instance uniq_bor_wf κ ty `{!TyWf ty} : TyWf (uniq_bor κ ty) :=
-    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty.(ty_outlives_E) κ }.
+    { ty_lfts := [κ]; ty_wf_E := ty.(ty_wf_E) ++ ty_outlives_E ty κ }.
 
   Global Instance uniq_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.