Fixing the checker w.r.t. wrongly used abstract universe contexts.

It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.

This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.

6 files changed, 35 insertions, 130 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 92e94c1ab..22c843812 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -525,10 +525,10 @@ let check_positivity env_ar mind params nrecp inds =
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
 (* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity =
+let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity =
   let numchecked = ref 0 in
   let basic_check ev tp =
-    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp);
     numchecked := !numchecked + 1
   in
   let check_typ typ typ_env =
@@ -548,26 +548,27 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-let check_subtyping cumi paramsctxt env_ar inds =
+let check_subtyping cumi paramsctxt env inds =
+  let open Univ in
   let numparams = rel_context_nhyps paramsctxt in
-  let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
-  let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in
-  let dosubst = subst_univs_level_constr sbsubst in
-  let uctx = Univ.CumulativityInfo.univ_context cumi in
-  let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
-  let env = Environ.push_context uctx env_ar 
-  in
-  let env = Environ.push_context uctx_other env 
-  in
-  let env =  Environ.push_context 
-      (Univ.CumulativityInfo.subtyp_context cumi) env
-  in
+  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+      with the cumulativity constraints [ cumul_cst ]. *)
+  let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
+  let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+  let other_context = ACumulativityInfo.univ_context cumi in
+  let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
+  let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
+  let cumul_cst = UContext.constraints cumul_context in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.add_constraints cumul_cst env in
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
       | RegularArity { mind_user_arity = full_arity} ->
-        check_subtyping_arity_constructor env dosubst full_arity numparams true;
-        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+        check_subtyping_arity_constructor env inst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc
       | TemplateArity _ -> ()
     ) inds
     
@@ -579,10 +580,10 @@ let check_inductive env kn mib =
   (* check mind_constraints: should be consistent with env *)
   let ind_ctx =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> ctx
-    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *)
+    | Polymorphic_ind auctx -> Univ.AUContext.repr auctx
     | Cumulative_ind cumi -> 
-      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+      Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
   in
   let env = Environ.push_context ind_ctx env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -606,8 +607,7 @@ let check_inductive env kn mib =
     match mib.mind_universes with
     | Monomorphic_ind _ | Polymorphic_ind _ -> ()
     | Cumulative_ind acumi ->
-      check_subtyping 
-        (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets
+      check_subtyping acumi params env_ar mib.mind_packets
   in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 15e9ae295..4948f6008 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,22 +26,21 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
-  let env', u =
+  (** [env'] contains De Bruijn universe variables *)
+  let env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+    | Monomorphic_const ctx -> push_context ~strict:true ctx env
     | Polymorphic_const auctx ->
-      let ctx = Univ.instantiate_univ_context auctx in
-      push_context ~strict:false ctx env, Univ.UContext.instance ctx
+      let ctx = Univ.AUContext.repr auctx in
+      push_context ~strict:false ctx env
   in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
-        let ty = subst_instance_constr u ty in
         let ty', cu = refresh_arity ty in
         let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
-        assert(Univ.Instance.is_empty u);
         let _ = check_ctxt env' ctxt in
         check_polymorphic_arity env' ctxt par;
 	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
@@ -49,7 +48,6 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
-      let bd = subst_instance_constr u bd in
       (match cb.const_proj with 
       | None -> let j = infer envty bd in
 		  conv_leq envty j ty
diff --git a/checker/term.ml b/checker/term.ml
index 9bcb15bc7..5995dfcc6 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -447,37 +447,3 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
-
-let subst_univs_level_constr subst c =
-  if Univ.is_empty_level_subst subst then c
-  else 
-    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
-    let changed = ref false in
-    let rec aux t = 
-      match t with
-      | Const (c, u) -> 
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Const (c, u'))
-      | Ind (i, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-	  let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Ind (i, u'))
-      | Construct (c, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Construct (c, u'))
-      | Sort (Type u) -> 
-         let u' = Univ.subst_univs_level_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; Sort (sort_of_univ u'))
-      | _ -> map_constr aux t
-    in
-    let c' = aux c in
-      if !changed then c' else c
diff --git a/checker/term.mli b/checker/term.mli
index ccf5b59e0..679a56ee4 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -57,4 +57,3 @@ val eq_constr : constr -> constr -> bool
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Univ.universe_instance -> constr -> constr
 val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
-val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
diff --git a/checker/univ.ml b/checker/univ.ml
index 2cd4252b2..e3abc436f 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1075,6 +1075,7 @@ module Instance : sig
     val check_eq : t check_function
     val length : t -> int
     val append : t -> t -> t
+    val of_array : Level.t array -> t
 end = 
 struct
   type t = Level.t array
@@ -1157,7 +1158,9 @@ struct
   let length = Array.length
 
   let append = Array.append
-  
+
+  let of_array i = i
+
 end
 
 (** Substitute instance inst for ctx in csts *)
@@ -1231,43 +1234,11 @@ module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
-  let make x =
-    if (Array.length (UContext.instance (snd x))) =
-       (Array.length (UContext.instance (fst x))) * 2 then x
-    else anomaly (Pp.str "Invalid subtyping information encountered!")
-
-  let empty = (UContext.empty, UContext.empty)
-
-  let halve_context ctx =
-    let len = Array.length ctx in
-    let halflen = len / 2 in
-    ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen))
-
   let univ_context (univcst, subtypcst) = univcst
   let subtyp_context (univcst, subtypcst) = subtypcst
 
-  let create_trivial_subtyping ctx ctx' =
-    CArray.fold_left_i
-      (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
-      Constraint.empty ctx
-
-  let from_universe_context univcst freshunivs =
-    let inst = (UContext.instance univcst) in
-    assert (Array.length freshunivs = Array.length inst);
-    (univcst, UContext.make (Array.append inst freshunivs,
-                             create_trivial_subtyping inst freshunivs))
-
-  let subtyping_other_instance (univcst, subtypcst) =
-    let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
-  
-  let subtyping_susbst (univcst, subtypcst) =
-    let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in
-    Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
-
 end
 
-type cumulativity_info = CumulativityInfo.t
-
 module ACumulativityInfo = CumulativityInfo
 type abstract_cumulativity_info = ACumulativityInfo.t
 
@@ -1315,13 +1286,6 @@ let subst_univs_level_universe subst u =
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_cumulativity_info (ctx, ctx') = 
-  (instantiate_univ_context ctx, instantiate_univ_context ctx')
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 01df46fa1..7f5aa7626 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,8 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val var : int -> t
+
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
   
@@ -179,6 +181,8 @@ sig
   val length : t -> int
   (** Compute the length of the instance  *)
 
+  val of_array : Level.t array -> t
+
   val append : t -> t -> t
   (** Append two universe instances *)
 end
@@ -208,7 +212,6 @@ module AUContext :
 sig
   type t
 
-  val instance : t -> Instance.t
   val size : t -> int
 
   val instantiate : Instance.t -> t -> Constraint.t
@@ -218,27 +221,6 @@ end
 
 type abstract_universe_context = AUContext.t
 
-module CumulativityInfo :
-sig
-  type t
-
-  val make : universe_context * universe_context -> t
-
-  val empty : t
-
-  val univ_context : t -> universe_context
-  val subtyp_context : t -> universe_context
-
-  val from_universe_context : universe_context -> universe_instance -> t
-
-  val subtyping_other_instance : t -> universe_instance
-  
-  val subtyping_susbst : t -> universe_level_subst
-
-end
-
-type cumulativity_info = CumulativityInfo.t
-
 module ACumulativityInfo :
 sig
   type t
@@ -284,10 +266,6 @@ val subst_instance_universe : universe_instance -> universe -> universe
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
 
-(** Get the instantiated graph. *)
-val instantiate_univ_context : abstract_universe_context -> universe_context
-val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
-
 (** Build the relative instance corresponding to the context *)
 val make_abstract_instance : abstract_universe_context -> universe_instance