1 files changed, 273 insertions, 323 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09f884ec..3158db52 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
@@ -31,133 +33,6 @@ open Util
    union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
-module type Hashconsed =
-sig
-  type t
-  val hash : t -> int
-  val eq : t -> t -> bool
-  val hcons : t -> t
-end
-
-module HashedList (M : Hashconsed) :
-sig
-  type t = private Nil | Cons of M.t * int * t
-  val nil : t
-  val cons : M.t -> t -> t
-end =
-struct
-  type t = Nil | Cons of M.t * int * t
-  module Self =
-  struct
-    type _t = t
-    type t = _t
-    type u = (M.t -> M.t)
-    let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let eq l1 l2 = match l1, l2 with
-    | Nil, Nil -> true
-    | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
-    | _ -> false
-    let hashcons hc = function
-    | Nil -> Nil
-    | Cons (x, h, l) -> Cons (hc x, h, l)
-  end
-  module Hcons = Hashcons.Make(Self)
-  let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons
-  (** No recursive call: the interface guarantees that all HLists from this
-      program are already hashconsed. If we get some external HList, we can
-      still reconstruct it by traversing it entirely. *)
-  let nil = Nil
-  let cons x l =
-    let h = M.hash x in
-    let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in
-    let h = Hashset.Combine.combine h hl in
-    hcons (Cons (x, h, l))
-end
-
-module HList = struct
-
-  module type S = sig
-    type elt
-    type t = private Nil | Cons of elt * int * t
-    val hash : t -> int
-    val nil : t
-    val cons : elt -> t -> t
-    val tip : elt -> t
-    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-    val map : (elt -> elt) -> t -> t
-    val smartmap : (elt -> elt) -> t -> t
-    val exists : (elt -> bool) -> t -> bool
-    val for_all : (elt -> bool) -> t -> bool
-    val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
-    val mem : elt -> t -> bool
-    val remove : elt -> t -> t
-    val to_list : t -> elt list
-    val compare : (elt -> elt -> int) -> t -> t -> int
-  end
-
-  module Make (H : Hashconsed) : S with type elt = H.t =
-  struct
-  type elt = H.t
-  include HashedList(H)
-
-  let hash = function Nil -> 0 | Cons (_, h, _) -> h
-
-  let tip e = cons e nil
-
-  let rec fold f l accu = match l with
-  | Nil -> accu
-  | Cons (x, _, l) -> fold f l (f x accu)
-
-  let rec map f = function
-  | Nil -> nil
-  | Cons (x, _, l) -> cons (f x) (map f l)
-
-  let smartmap = map
-  (** Apriori hashconsing ensures that the map is equal to its argument *)
-
-  let rec exists f = function
-  | Nil -> false
-  | Cons (x, _, l) -> f x || exists f l
-
-  let rec for_all f = function
-  | Nil -> true
-  | Cons (x, _, l) -> f x && for_all f l
-
-  let rec for_all2 f l1 l2 = match l1, l2 with
-  | Nil, Nil -> true
-  | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2
-  | _ -> false
-
-  let rec to_list = function
-  | Nil -> []
-  | Cons (x, _, l) -> x :: to_list l
-
-  let rec remove x = function
-  | Nil -> nil
-  | Cons (y, _, l) ->
-    if H.eq x y then l
-    else cons y (remove x l)
-
-  let rec mem x = function
-  | Nil -> false
-  | Cons (y, _, l) -> H.eq x y || mem x l
-
-  let rec compare cmp l1 l2 = match l1, l2 with
-  | Nil, Nil -> 0
-  | Cons (x1, h1, l1), Cons (x2, h2, l2) ->
-    let c = Int.compare h1 h2 in
-    if c == 0 then
-      let c = cmp x1 x2 in
-      if c == 0 then
-        compare cmp l1 l2
-      else c
-    else c
-  | Cons _, Nil -> 1
-  | Nil, Cons _ -> -1
-
-  end
-end
-
 module RawLevel =
 struct
   open Names
@@ -248,8 +123,7 @@ module Level = struct
   (** Hashcons on levels + their hash *)
 
   module Self = struct
-    type _t = t
-    type t = _t
+    type nonrec t = t
     type u = unit
     let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
@@ -320,6 +194,10 @@ module Level = struct
 
   let make m n = make (Level (n, Names.DirPath.hcons m))
 
+  let name u =
+    match data u with
+    | Level (n, d) -> Some (d, n)
+    | _ -> None
 end
 
 (** Level maps *)
@@ -390,12 +268,11 @@ struct
   module Expr = 
   struct
     type t = Level.t * int
-    type _t = t
-	
+
     (* Hashing of expressions *)
     module ExprHash = 
     struct
-      type t = _t
+      type t = Level.t * int
       type u = Level.t -> Level.t
       let hashcons hdir (b,n as x) = 
 	let b' = hdir b in 
@@ -409,25 +286,12 @@ struct
 
     end
 
-    module HExpr = 
-    struct 
-
-      module H = Hashcons.Make(ExprHash)
-
-      type t = ExprHash.t
-
-      let hcons =
-	Hashcons.simple_hcons H.generate H.hcons Level.hcons
-      let hash = ExprHash.hash
-      let eq x y = x == y ||
-	(let (u,n) = x and (v,n') = y in
-	   Int.equal n n' && Level.equal u v)
-
-    end
+    module H = Hashcons.Make(ExprHash)
 
-    let hcons = HExpr.hcons
+    let hcons =
+      Hashcons.simple_hcons H.generate H.hcons Level.hcons
 
-    let make l = hcons (l, 0)
+    let make l = (l, 0)
 
     let compare u v =
       if u == v then 0
@@ -436,14 +300,10 @@ struct
 	  if Int.equal n n' then Level.compare x x'
 	  else n - n'
 
-    let prop = make Level.prop
-    let set = make Level.set
+    let prop = hcons (Level.prop, 0)
+    let set = hcons (Level.set, 0)
     let type1 = hcons (Level.set, 1)
 
-    let is_prop = function
-      | (l,0) -> Level.is_prop l
-      | _ -> false
-	
     let is_small = function
       | (l,0) -> Level.is_small l
       | _ -> false
@@ -452,6 +312,8 @@ struct
       (let (u,n) = x and (v,n') = y in
 	 Int.equal n n' && Level.equal u v)
 
+    let hash = ExprHash.hash
+
     let leq (u,n) (v,n') =
       let cmp = Level.compare u v in
 	if Int.equal cmp 0 then n <= n'
@@ -461,13 +323,13 @@ struct
 
     let successor (u,n) =
       if Level.is_prop u then type1
-      else hcons (u, n + 1)
+      else (u, n + 1)
 
     let addn k (u,n as x) = 
       if k = 0 then x 
       else if Level.is_prop u then
-	hcons (Level.set,n+k)
-      else hcons (u,n+k)
+	(Level.set,n+k)
+      else (u,n+k)
 
     type super_result =
 	SuperSame of bool
@@ -481,19 +343,16 @@ struct
        returning [SuperSame] if they refer to the same level at potentially different
        increments or [SuperDiff] if they are different. The booleans indicate if the
        left expression is "smaller" than the right one in both cases. *)
-    let super (u,n as x) (v,n' as y) =
+    let super (u,n) (v,n') =
       let cmp = Level.compare u v in
 	if Int.equal cmp 0 then SuperSame (n < n')
 	else
-	  match x, y with
-	  | (l,0), (l',0) ->
-	     let open RawLevel in
-	     (match Level.data l, Level.data l' with
-	      | Prop, Prop -> SuperSame false
-	      | Prop, _ -> SuperSame true
-	      | _, Prop -> SuperSame false
-	      | _, _ -> SuperDiff cmp)
-	  | _, _ -> SuperDiff cmp
+          let open RawLevel in
+          match Level.data u, n, Level.data v, n' with
+          | Prop, _, Prop, _ -> SuperSame (n < n')
+          | Prop, 0, _, _ -> SuperSame true
+          | _, _, Prop, 0 -> SuperSame false
+          | _, _, _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -519,71 +378,63 @@ struct
       let v' = f v in 
 	if v' == v then x
 	else if Level.is_prop v' && n != 0 then
-	  hcons (Level.set, n)
-	else hcons (v', n)
+	  (Level.set, n)
+	else (v', n)
 
   end
-    
-  let compare_expr = Expr.compare
 
-  module Huniv = HList.Make(Expr.HExpr)
-  type t = Huniv.t
-  open Huniv
-    
-  let equal x y = x == y || 
-    (Huniv.hash x == Huniv.hash y && 
-       Huniv.for_all2 Expr.equal x y)
+  type t = Expr.t list
 
-  let hash = Huniv.hash
+  let tip l = [l]
+  let cons x l = x :: l
 
-  let compare x y =
-    if x == y then 0
-    else 
-      let hx = Huniv.hash x and hy = Huniv.hash y in
-      let c = Int.compare hx hy in 
-	if c == 0 then
-	  Huniv.compare (fun e1 e2 -> compare_expr e1 e2) x y
-	else c
+  let rec hash = function
+  | [] -> 0
+  | e :: l -> Hashset.Combine.combinesmall (Expr.ExprHash.hash e) (hash l)
 
-  let rec hcons = function
-  | Nil -> Huniv.nil
-  | Cons (x, _, l) -> Huniv.cons x (hcons l)
+  let equal x y = x == y || List.equal Expr.equal x y
 
-  let make l = Huniv.tip (Expr.make l)
-  let tip x = Huniv.tip x
+  let compare x y = if x == y then 0 else List.compare Expr.compare x y
+
+  module Huniv = Hashcons.Hlist(Expr)
+
+  let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons
+
+  let make l = tip (Expr.make l)
+  let tip x = tip x
 
   let pr l = match l with
-    | Cons (u, _, Nil) -> Expr.pr u
+    | [u] -> Expr.pr u
     | _ -> 
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma Expr.pr (to_list l)) ++
+	(prlist_with_sep pr_comma Expr.pr l) ++
         str ")"
 
   let pr_with f l = match l with
-    | Cons (u, _, Nil) -> Expr.pr_with f u
+    | [u] -> Expr.pr_with f u
     | _ -> 
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++
+	(prlist_with_sep pr_comma (Expr.pr_with f) l) ++
         str ")"
 
   let is_level l = match l with
-    | Cons (l, _, Nil) -> Expr.is_level l
+    | [l] -> Expr.is_level l
     | _ -> false
 
   let rec is_levels l = match l with
-    | Cons (l, _, r) -> Expr.is_level l && is_levels r
-    | Nil -> true
+    | l :: r -> Expr.is_level l && is_levels r
+    | [] -> true
 
   let level l = match l with
-    | Cons (l, _, Nil) -> Expr.level l
+    | [l] -> Expr.level l
     | _ -> None
 
   let levels l = 
-    fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty
+    List.fold_left (fun acc x -> LSet.add (Expr.get_level x) acc) LSet.empty l
 
   let is_small u = 
     match u with
-    | Cons (l, _, Nil) -> Expr.is_small l
+    | [l] -> Expr.is_small l
     | _ -> false
 
   (* The lower predicative level of the hierarchy that contains (impredicative)
@@ -605,16 +456,16 @@ struct
   let super l = 
     if is_small l then type1
     else
-      Huniv.map (fun x -> Expr.successor x) l
+      List.smartmap (fun x -> Expr.successor x) l
 
   let addn n l =
-    Huniv.map (fun x -> Expr.addn n x) l
+    List.smartmap (fun x -> Expr.addn n x) l
 
   let rec merge_univs l1 l2 =
     match l1, l2 with
-    | Nil, _ -> l2
-    | _, Nil -> l1
-    | Cons (h1, _, t1), Cons (h2, _, t2) ->
+    | [], _ -> l2
+    | _, [] -> l1
+    | h1 :: t1, h2 :: t2 ->
        let open Expr in
        (match super h1 h2 with
 	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
@@ -627,7 +478,7 @@ struct
   let sort u =
     let rec aux a l = 
       match l with
-      | Cons (b, _, l') ->
+      | b :: l' ->
 	let open Expr in
         (match super a b with
 	 | SuperSame false -> aux a l'
@@ -635,22 +486,23 @@ struct
 	 | SuperDiff c ->
 	    if c <= 0 then cons a l
 	    else cons b (aux a l'))
-      | Nil -> cons a l
+      | [] -> cons a l
     in 
-      fold (fun a acc -> aux a acc) u nil
-	
+      List.fold_right (fun a acc -> aux a acc) u []
+
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y
 
-  let empty = nil
+  let empty = []
 
-  let exists = Huniv.exists
+  let exists = List.exists
 
-  let for_all = Huniv.for_all
+  let for_all = List.for_all
 
-  let smartmap = Huniv.smartmap
+  let smartmap = List.smartmap
 
+  let map = List.map
 end
 
 type universe = Universe.t
@@ -729,8 +581,11 @@ struct
       pp_std ++ prl u1 ++ pr_constraint_type op ++
 	prl u2 ++ fnl () )  c (str "")
 
+  let universes_of c =
+    fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
 end
 
+let universes_of_constraints = Constraint.universes_of
 let empty_constraint = Constraint.empty
 let union_constraint = Constraint.union
 let eq_constraint = Constraint.equal
@@ -785,7 +640,7 @@ let enforce_eq_level u v c =
 let enforce_eq u v c =
   match Universe.level u, Universe.level v with
     | Some u, Some v -> enforce_eq_level u v c
-    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables")
+    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables.")
 
 let check_univ_eq u v = Universe.equal u v
 
@@ -805,13 +660,13 @@ let constraint_add_leq v u c =
       else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
 	if Level.equal x y then (* u+(k+1) <= u *)
 	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
       else if j = 0 then
 	Constraint.add (x,Le,y) c
       else (* j >= 1 *) (* m = n + k, u <= v+k *)
 	if Level.equal x y then c (* u <= u+k, trivial *)
 	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+        else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
 	  
 let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
 
@@ -819,13 +674,7 @@ let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  let open Universe.Huniv in
-  let rec aux acc v =
-  match v with
-  | Cons (v, _, l) ->
-    aux (fold (fun u -> constraint_add_leq u v) u c) l
-  | Nil -> acc
-  in aux c v
+  List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
@@ -834,21 +683,16 @@ let enforce_leq u v c =
 let enforce_leq_level u v c =
   if Level.equal u v then c else Constraint.add (u,Le,v) c
 
-let enforce_univ_constraint (u,d,v) =
-  match d with
-  | Eq -> enforce_eq u v
-  | Le -> enforce_leq u v
-  | Lt -> enforce_leq (super u) v
-
 (* Miscellaneous functions to remove or test local univ assumed to
    occur in a universe *)
 
-let univ_level_mem u v = Huniv.mem (Expr.make u) v
+let univ_level_mem u v =
+  List.exists (fun (l, n) -> Int.equal n 0 && Level.equal u l) v
 
 let univ_level_rem u v min = 
   match Universe.level v with
   | Some u' -> if Level.equal u u' then min else v
-  | None -> Huniv.remove (Universe.Expr.make u) v
+  | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v
 
 (* Is u mentionned in v (or equals to v) ? *)
 
@@ -865,15 +709,55 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-let level_subst_of f = 
-  fun l -> 
-    try let u = f l in 
-	  match Universe.level u with
-	  | None -> l
-	  | Some l -> l
-    with Not_found -> l
-     
-module Instance : sig 
+module Variance =
+struct
+  (** 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
+
+  let sup x y =
+    match x, y with
+    | Irrelevant, s | s, Irrelevant -> s
+    | 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 "+"
+    | Invariant -> str "="
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> enforce_leq_level u u' csts
+    | Invariant -> enforce_eq_level u u' csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> enforce_eq_level u u' csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module Instance : sig
     type t = Level.t array
 
     val empty : t
@@ -893,7 +777,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+    val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
@@ -903,8 +787,7 @@ struct
 
   module HInstancestruct =
   struct
-    type _t = t
-    type t = _t
+    type nonrec t = t
     type u = Level.t -> Level.t
 
     let hashcons huniv a = 
@@ -970,8 +853,12 @@ struct
 
   let levels x = LSet.of_array x
 
-  let pr =
-    prvect_with_sep spc
+  let pr prl ?variance =
+    let ppu i u =
+      let v = Option.map (fun v -> v.(i)) variance in
+      pr_opt_no_spc Variance.pr v ++ prl u
+    in
+    prvecti_with_sep spc ppu
 
   let equal t u = 
     t == u ||
@@ -986,9 +873,37 @@ let enforce_eq_instances x y =
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with")
-		 (Pp.str " instances of different lengths"));
+		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
+let enforce_eq_variance_instances = Variance.eq_constraints
+let enforce_leq_variance_instances = Variance.leq_constraints
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1010,9 +925,9 @@ struct
   let empty = (Instance.empty, Constraint.empty)
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
 
-  let pr prl (univs, cst as ctx) =
+  let pr prl ?variance (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -1032,6 +947,69 @@ end
 type universe_context = UContext.t
 let hcons_universe_context = UContext.hcons
 
+module AUContext =
+struct
+  include UContext
+
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
+
+type abstract_universe_context = AUContext.t
+let hcons_abstract_universe_context = AUContext.hcons
+
+(** Universe info for cumulative inductive types: A context of
+   universe levels with universe constraints, representing local
+   universe variables and constraints, together with an array of
+   Variance.t.
+
+    This data structure maintains the invariant that the variance
+   array has the same length as the universe instance. *)
+module CumulativityInfo =
+struct
+  type t = universe_context * Variance.t array
+
+  let make x =
+    if (Instance.length (UContext.instance (fst x))) =
+       (Array.length (snd x)) then x
+    else anomaly (Pp.str "Invalid subtyping information encountered!")
+
+  let empty = (UContext.empty, [||])
+  let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
+
+  let pr prl (univs, variance) =
+    UContext.pr prl ~variance univs
+
+  let hcons (univs, variance) = (* should variance be hconsed? *)
+    (UContext.hcons univs, variance)
+
+  let univ_context (univs, subtypcst) = univs
+  let variance (univs, variance) = variance
+
+  (** This function takes a universe context representing constraints
+     of an inductive and produces a CumulativityInfo.t with the
+     trivial subtyping relation. *)
+  let from_universe_context univs =
+    (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
+
+  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+
+end
+
+type cumulativity_info = CumulativityInfo.t
+let hcons_cumulativity_info = CumulativityInfo.hcons
+
+module ACumulativityInfo = CumulativityInfo
+
+type abstract_cumulativity_info = ACumulativityInfo.t
+let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
+
 (** A set of universes with universe constraints.
     We linearize the set to a list after typechecking. 
     Beware, representation could change.
@@ -1091,6 +1069,7 @@ struct
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
 
+  let size (univs,_) = LSet.cardinal univs
 end
 
 type universe_context_set = ContextSet.t
@@ -1136,6 +1115,9 @@ let subst_univs_level_constraints subst csts =
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
     csts Constraint.empty 
 
+let subst_univs_level_abstract_universe_context subst (inst, csts) =
+  inst, subst_univs_level_constraints subst csts
+
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1146,7 +1128,7 @@ let subst_univs_expr_opt fn (l,n) =
 
 let subst_univs_universe fn ul =
   let subst, nosubst = 
-    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+    List.fold_right (fun u (subst,nosubst) -> 
       try let a' = subst_univs_expr_opt fn u in
 	    (a' :: subst, nosubst)
       with Not_found -> (subst, u :: nosubst))
@@ -1157,59 +1139,9 @@ let subst_univs_universe fn ul =
       let substs = 
 	List.fold_left Universe.merge_univs Universe.empty subst
       in
-	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
+	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
 	  substs nosubst
 
-let subst_univs_level fn l = 
-  try Some (fn l)
-  with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
-  let u' = subst_univs_level fn u in
-  let v' = subst_univs_level fn v in
-  match u', v' with
-  | None, None -> Constraint.add c cstrs
-  | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
-  | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
-  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
-  Constraint.fold 
-    (fun c cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty 
-
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
-
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u csts
-
 let make_instance_subst i = 
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
@@ -1222,16 +1154,35 @@ let make_inverse_instance_subst i =
       LMap.add (Level.var i) l acc)
       LMap.empty arr
 
-let abstract_universes poly ctx =
+let make_abstract_instance (ctx, _) = 
+  Array.mapi (fun i l -> Level.var i) ctx
+
+let abstract_universes ctx =
   let instance = UContext.instance ctx in
-    if poly then
-      let subst = make_instance_subst instance in
-      let cstrs = subst_univs_level_constraints subst 
-	(UContext.constraints ctx)
-      in
-      let ctx = UContext.make (instance, cstrs) in
-	subst, ctx
-    else empty_level_subst, ctx
+  let subst = make_instance_subst instance in
+  let cstrs = subst_univs_level_constraints subst 
+      (UContext.constraints ctx)
+  in
+  let ctx = UContext.make (instance, cstrs) in
+  instance, ctx
+
+let abstract_cumulativity_info (univs, variance) =
+  let subst, univs = abstract_universes univs in
+  subst, (univs, variance)
+
+let rec compact_univ s vars i u =
+  match u with
+  | [] -> (s, List.rev vars)
+  | (lvl, _) :: u ->
+    match Level.var_index lvl with
+    | Some k when not (LMap.mem lvl s) ->
+      let lvl' = Level.var i in
+      compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u
+    | _ -> compact_univ s vars i u
+
+let compact_univ u =
+  let (s, s') = compact_univ LMap.empty [] 0 u in
+  (subst_univs_level_universe s u, s')
 
 (** Pretty-printing *)
 
@@ -1239,6 +1190,12 @@ let pr_constraints prl = Constraint.pr prl
 
 let pr_universe_context = UContext.pr
 
+let pr_cumulativity_info = CumulativityInfo.pr
+
+let pr_abstract_universe_context = AUContext.pr
+
+let pr_abstract_cumulativity_info = ACumulativityInfo.pr
+
 let pr_universe_context_set = ContextSet.pr
 
 let pr_universe_subst = 
@@ -1287,10 +1244,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 let compare_levels = Level.compare
 let eq_levels = Level.equal
 let equal_universes = Universe.equal
-
-
-let subst_instance_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_constraints
-  else subst_instance_constraints