Merge PR #6740: Adding a sanity check on inductive variance subtyping.

7 files changed, 54 insertions, 1 deletions

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 98a9c8250..77201c25b 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -108,6 +108,14 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       let env = check_polymorphic_instance error env auctx auctx' in
       env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
+      (** Currently there is no way to control variance of inductive types, but
+          just in case we require that they are in a subtyping relation. *)
+      let () =
+        let v = Univ.ACumulativityInfo.variance cumi in
+        let v' = Univ.ACumulativityInfo.variance cumi' in
+        if not (Array.for_all2 Univ.Variance.check_subtype v' v) then
+          CErrors.anomaly Pp.(str "Variance mismatch for " ++ MutInd.print kn)
+      in
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
       let env = check_polymorphic_instance error env auctx auctx' in
diff --git a/checker/univ.ml b/checker/univ.ml
index 46b3ce680..ebc37bc10 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1011,6 +1011,13 @@ struct
      A'] as opposed to [A' <= A]. *)
   type t = Irrelevant | Covariant | Invariant
 
+  let check_subtype x y = match x, y with
+  | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+  | Irrelevant, Covariant -> false
+  | (Covariant | Invariant), Covariant -> true
+  | (Irrelevant | Covariant), Invariant -> false
+  | Invariant, Invariant -> true
+
   let leq_constraint csts variance u u' =
     match variance with
     | Irrelevant -> csts
diff --git a/checker/univ.mli b/checker/univ.mli
index 8c0685e0b..32e48f593 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -225,7 +225,7 @@ sig
      case because [forall x : A, B <= forall x : A', B'] requires [A =
      A'] as opposed to [A' <= A]. *)
   type t = Irrelevant | Covariant | Invariant
-
+  val check_subtype : t -> t -> bool
   val leq_constraints : t array -> Instance.t constraint_function
   val eq_constraints : t array -> Instance.t constraint_function
 end
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d0d5cb1d5..e95d5d2b5 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -118,6 +118,15 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       let env = check_polymorphic_instance error env auctx auctx' in
       env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
+      (** Currently there is no way to control variance of inductive types, but
+          just in case we require that they are in a subtyping relation. *)
+      let () =
+        let v = ACumulativityInfo.variance cumi in
+        let v' = ACumulativityInfo.variance cumi' in
+        if not (Array.for_all2 Variance.check_subtype v' v) then
+          CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++
+            str " is not compatible with the one of " ++ KerName.print kn2)
+      in
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
       let env = check_polymorphic_instance error env auctx auctx' in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fbb047364..c42b66749 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -759,6 +759,13 @@ struct
     | Invariant, _ | _, Invariant -> Invariant
     | Covariant, Covariant -> Covariant
 
+  let check_subtype x y = match x, y with
+  | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+  | Irrelevant, Covariant -> false
+  | (Covariant | Invariant), Covariant -> true
+  | (Irrelevant | Covariant), Invariant -> false
+  | Invariant, Invariant -> true
+
   let pr = function
     | Irrelevant -> str "*"
     | Covariant -> str "+"
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c45ebe21c..74d1bfd3a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -253,6 +253,9 @@ sig
      A'] as opposed to [A' <= A]. *)
   type t = Irrelevant | Covariant | Invariant
 
+  (** [check_subtype x y] holds if variance [y] is also an instance of [x] *)
+  val check_subtype : t -> t -> bool
+
   val sup : t -> t -> t
 
   val pr : t -> Pp.t
diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v
new file mode 100644
index 000000000..654b86cb4
--- /dev/null
+++ b/test-suite/modules/cumpoly.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+(** Check that variance subtyping is respected. The signature T is asking for
+    invariance, while M provide an irrelevant implementation, which is deemed
+    legit.
+
+    There is currently no way to go the other way around, so it's not possible
+    to generate a counter-example that should fail with the wrong subtyping.
+*)
+
+Module Type T.
+Parameter t@{i|Set <= i} : Type@{i}.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End T.
+
+Module M : T.
+Definition t@{i|Set <= i} : Type@{i} := nat.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End M.