Simplify prood of sum_proper. Define LstCopy.

theories/typing/product.v

@@ -127,9 +127,7 @@ Section product.
   Global Instance product_proper E L:
     Proper (Forall2 (eqtype E L) ==> eqtype E L) product.
   Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
-  (* FIXME : this instance is never going to be used, because Forall is
-     not a typeclass. *)
-  Global Instance product_copy tys : Forall Copy tys → Copy (product tys).
+  Global Instance product_copy tys : LstCopy tys → Copy (product tys).
   Proof. induction 1; apply _. Qed.
 End product.
 

theories/typing/sum.v

@@ -110,18 +110,11 @@ Section sum.
   Global Instance sum_proper E L:
     Proper (Forall2 (eqtype E L) ==> eqtype E L) sum.
   Proof.
-    (* TODO: Isn't there sth. showing that Forall2 is monotnous wrt. the predicate? *)
-    intros tyl1 tyl2 Heq.
-    assert (Forall2 (subtype E L) tyl1 tyl2 ∧ Forall2 (subtype E L) tyl2 tyl1).
-    { induction Heq as [|???? Heq]; first done. destruct_and!.
-      destruct Heq. split; constructor; done. }
-    destruct_and!. split; apply sum_mono; done.
+    intros tyl1 tyl2 Heq; split; eapply sum_mono; [|rewrite -Forall2_flip];
+      (eapply Forall2_impl; [done|by intros ?? []]).
   Qed.
 
-  (* TODO : Make the Forall parameter a typeclass *)
-  (* TODO : This next step is suspuciously slow. *)
-  Global Instance sum_copy tyl :
-    Forall Copy tyl → Copy (sum tyl).
+  Global Instance sum_copy tyl: LstCopy tyl → Copy (sum tyl).
   Proof.
     intros HFA. split.
     - intros tid vl.
@@ -142,7 +135,7 @@ Section sum.
       rewrite -(heap_mapsto_vec_prop_op _ q' q'12); last (by intros; apply ty_size_eq).
       rewrite -!Qp_plus_assoc.
       rewrite -(heap_mapsto_vec_prop_op _ q' (q'11 + q'02)
-                                        (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
+            (list_max (map ty_size tyl) - (ty_size (nth i tyl ∅)))%nat); last first.
       { intros. iIntros (<-). iPureIntro. by rewrite minus_plus. }
       iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 >Hown2]".
       iDestruct "Htail" as "[Htail1 Htail2]".

theories/typing/type.v

@@ -42,16 +42,21 @@ Section type.
     }.
   Global Existing Instances ty_shr_persistent.
 
-  Class Copy (t : type) := {
-    copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
+  Class Copy (ty : type) := {
+    copy_persistent tid vl : PersistentP (ty.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
       mgmtE ∪ F ⊆ E →
-      lft_ctx -∗ t.(ty_shr) κ tid F l -∗
-        q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: t.(ty_own) tid ∗
-          (▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
+      lft_ctx -∗ ty.(ty_shr) κ tid F l -∗
+        q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty.(ty_own) tid ∗
+          (▷l ↦∗{q'}: ty.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)
   }.
   Global Existing Instances copy_persistent.
 
+  Class LstCopy (tys : list type) := lst_copy : Forall Copy tys.
+  Global Instance lst_copy_nil : LstCopy [] := List.Forall_nil _.
+  Global Instance lst_copy_cons ty tys :
+    Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
+
   (* We are repeating the typeclass parameter here jsut to make sure
      that simple_type does depend on it. Otherwise, the coercion defined
      bellow will not be acceptable by Coq. *)