Simplification: cumulativity information is variance information.

Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.

As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).

Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie

         Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
         Print Foo.

gives

        Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
          { foo : Type@{i} -> Type@{j} }
          (* =i +j *k |=  *)

1 files changed, 14 insertions, 1 deletions

diff --git a/checker/univ.mli b/checker/univ.mli
index 21c94d952..8c0685e0b 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -218,12 +218,25 @@ end
 
 type abstract_universe_context = AUContext.t
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val leq_constraints : t array -> Instance.t constraint_function
+  val eq_constraints : t array -> Instance.t constraint_function
+end
+
+
 module ACumulativityInfo :
 sig
   type t
 
   val univ_context : t -> abstract_universe_context
-  val subtyp_context : t -> abstract_universe_context
+  val variance : t -> Variance.t array
 
 end