From 104b8849e64ea9fbd1ba36548551074c6d382e36 Mon Sep 17 00:00:00 2001
From: Irene Yoon <ey222@cornell.edu>
Date: Fri, 18 Mar 2022 22:15:07 +0000
Subject: [PATCH] GFunctors changed to a record

---
 iris/base_logic/lib/iprop.v | 20 +++++++++++++-------
 tests/iprop.ref             |  0
 tests/iprop.v               | 19 +++++++++++++++++++
 3 files changed, 32 insertions(+), 7 deletions(-)
 create mode 100644 tests/iprop.ref
 create mode 100644 tests/iprop.v

diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 1b2c47ce1..fb2663030 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -37,11 +37,16 @@ of [gFunctor]s.
 
 Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
 alternative way to avoid universe inconsistencies with respect to the universe
-monomorphic [list] type. *)
-Definition gFunctors := { n : nat & fin n → gFunctor }.
+monomorphic [list] type.
 
-Definition gid (Σ : gFunctors) := fin (projT1 Σ).
-Definition gFunctors_lookup (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
+Defining [gFunctors] as a dependent record instead of a [sigT] avoids other
+universe inconsistencies. *)
+Record gFunctors := GFunctors {
+  gFunctors_len : nat;
+  gFunctors_lookup : fin gFunctors_len → gFunctor
+}.
+
+Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).
 
 Definition gname := positive.
 Canonical Structure gnameO := leibnizO gname.
@@ -55,13 +60,14 @@ Definition iResF (Σ : gFunctors) : urFunctor :=
 functors, and the append operator on lists of functors. These are used to
 compose [gFunctors] out of smaller pieces. *)
 Module gFunctors.
-  Definition nil : gFunctors := existT 0 (fin_0_inv _).
+  Definition nil : gFunctors := GFunctors 0 (fin_0_inv _).
 
   Definition singleton (F : gFunctor) : gFunctors :=
-    existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
+    GFunctors 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
 
   Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
-    existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)).
+    GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
+              (fin_plus_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
 End gFunctors.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
diff --git a/tests/iprop.ref b/tests/iprop.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/iprop.v b/tests/iprop.v
new file mode 100644
index 000000000..49d6cb4a5
--- /dev/null
+++ b/tests/iprop.v
@@ -0,0 +1,19 @@
+(** Make sure these universe constraints do not conflict with Iris's definition
+of [gFunctors]:
+See [!782](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/782) *)
+
+From Coq Require Import Logic.Eqdep.
+
+(** A [sigT] that is partially applied and template-polymorphic causes universe
+inconsistency errors, which is why [sigT] should be avoided for the definition
+of [gFunctors].
+
+The following constructs a partially applied [sigT] that generates bad universe
+constraints. This causes a universe inconsistency when [gFunctors] are
+to be defined with [sigT]. *)
+Definition foo :=
+  eq_dep
+    ((Type -> Type) -> Type)
+    (sigT (A:=Type -> Type)).
+
+From iris.base_logic Require Import iprop.
-- 
GitLab