Merge PR #9027: Refactor checking of inductive types

Ack-by: SkySkimmer
Reviewed-by: mattam82
Ack-by: maximedenes
Ack-by: ppedrot

9 files changed, 427 insertions, 459 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 38a428d9a1..77820a301e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -238,6 +238,13 @@ let is_impredicative_set env =
   | ImpredicativeSet -> true
   | _ -> false
 
+let is_impredicative_sort env = function
+  | Sorts.Prop -> true
+  | Sorts.Set -> is_impredicative_set env
+  | Sorts.Type _ -> false
+
+let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+
 let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8a2efb2477..6d4d3b282b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -98,6 +98,9 @@ val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
 
+val is_impredicative_sort : env -> Sorts.t -> bool
+val is_impredicative_univ : env -> Univ.Universe.t -> bool
+
 (** is the local context empty *)
 val empty_context : env -> bool
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
new file mode 100644
index 0000000000..6976b2019d
--- /dev/null
+++ b/kernel/indTyping.ml
@@ -0,0 +1,307 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Univ
+open Term
+open Constr
+open Declarations
+open Environ
+open Entries
+open Type_errors
+open Context.Rel.Declaration
+
+(** Check name unicity.
+    Redundant with safe_typing's add_field checks -> to remove?. *)
+
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
+let check_constructors_names =
+  let rec check idset = function
+    | [] -> idset
+    | c::cl ->
+        if Id.Set.mem c idset then
+          raise (InductiveError (SameNamesConstructors c))
+        else
+          check (Id.Set.add c idset) cl
+  in
+  check
+
+(* [mind_check_names mie] checks the names of an inductive types declaration,
+   and raises the corresponding exceptions when two types or two constructors
+   have the same name. *)
+
+let mind_check_names mie =
+  let rec check indset cstset = function
+    | [] -> ()
+    | ind::inds ->
+        let id = ind.mind_entry_typename in
+        let cl = ind.mind_entry_consnames in
+        if Id.Set.mem id indset then
+          raise (InductiveError (SameNamesTypes id))
+        else
+          let cstset' = check_constructors_names cstset cl in
+          check (Id.Set.add id indset) cstset' inds
+  in
+  check Id.Set.empty Id.Set.empty mie.mind_entry_inds
+(* The above verification is not necessary from the kernel point of
+  vue since inductive and constructors are not referred to by their
+  name, but only by the name of the inductive packet and an index. *)
+
+
+(************************************************************************)
+(************************** Cumulativity checking************************)
+(************************************************************************)
+
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env subst arcn numparams is_arity =
+  let numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp);
+    numchecked := !numchecked + 1
+  in
+  let check_typ typ typ_env =
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with Reduction.NotConvertible ->
+          CErrors.anomaly ~label:"bad inductive subtyping relation"
+            Pp.(str "Invalid subtyping relation")
+      end
+    | _ -> CErrors.anomaly Pp.(str "")
+  in
+  let typs, codom = Reduction.dest_prod env arcn in
+  let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+let check_cumulativity univs env_ar params data =
+  let numparams = Context.Rel.nhyps params in
+  let uctx = CumulativityInfo.univ_context univs in
+  let new_levels = Array.init (UContext.size uctx)
+      (fun i -> Level.(make (UGlobal.make DirPath.empty i)))
+  in
+  let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
+      LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
+  in
+  let dosubst = Vars.subst_univs_level_constr lmap in
+  let instance_other = Instance.of_array new_levels in
+  let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
+  let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+  let env = Environ.push_context uctx_other env_ar in
+  let subtyp_constraints =
+    CumulativityInfo.leq_constraints univs
+      (UContext.instance uctx) instance_other
+      Constraint.empty
+  in
+  let env = Environ.add_constraints subtyp_constraints env in
+  (* process individual inductive types: *)
+  List.iter (fun (arity,lc) ->
+        check_subtyping_arity_constructor env dosubst arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc)
+    data
+
+(************************************************************************)
+(************************** Type checking *******************************)
+(************************************************************************)
+
+type univ_info = { ind_squashed : bool;
+                   ind_min_univ : Universe.t option; (* Some for template *)
+                   ind_univ : Universe.t }
+
+let check_univ_leq env u info =
+  let ind_univ = info.ind_univ in
+  if type_in_type env || (UGraph.check_leq (universes env) u ind_univ)
+  then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
+  else if is_impredicative_univ env ind_univ
+  then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+    else raise (InductiveError BadUnivs)
+  else raise (InductiveError BadUnivs)
+
+let check_indices_matter env_params info indices =
+  let check_index d (info,env) =
+    let info = match d with
+      | LocalAssum (_,t) ->
+        (* could be retyping if it becomes available in the kernel *)
+        let tj = Typeops.infer_type env t in
+        check_univ_leq env (Sorts.univ_of_sort tj.utj_type) info
+      | LocalDef _ -> info
+    in
+    info, push_rel d env
+  in
+  if not (indices_matter env_params) then info
+  else fst (Context.Rel.fold_outside ~init:(info,env_params) check_index indices)
+
+(* env_ar contains the inductives before the current ones in the block, and no parameters *)
+let check_arity env_params env_ar ind =
+  let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
+  let indices, ind_sort = Reduction.dest_arity env_params arity in
+  let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in
+  let univ_info = {ind_squashed=false;ind_min_univ;ind_univ=Sorts.univ_of_sort ind_sort} in
+  let univ_info = check_indices_matter env_params univ_info indices in
+  (* We do not need to generate the universe of the arity with params;
+     if later, after the validation of the inductive definition,
+     full_arity is used as argument or subject to cast, an upper
+     universe will be generated *)
+  let arity = it_mkProd_or_LetIn arity (Environ.rel_context env_params) in
+  push_rel (LocalAssum (Name ind.mind_entry_typename, arity)) env_ar,
+  (arity, indices, univ_info)
+
+let check_constructor_univs env_ar_par univ_info (args,_) =
+  (* We ignore the output, positivity will check that it's the expected inductive type *)
+  (* NB: very similar to check_indices_matter but that will change with SProp *)
+  fst (Context.Rel.fold_outside ~init:(univ_info,env_ar_par) (fun d (univ_info,env) ->
+      let univ_info = match d with
+        | LocalDef _ -> univ_info
+        | LocalAssum (_,t) ->
+          (* could be retyping if it becomes available in the kernel *)
+          let tj = Typeops.infer_type env t in
+          check_univ_leq env (Sorts.univ_of_sort tj.utj_type) univ_info
+      in
+      univ_info, push_rel d env)
+      args)
+
+let check_constructors env_ar_par params lc (arity,indices,univ_info) =
+  let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in
+  let splayed_lc = Array.map (Reduction.dest_prod_assum env_ar_par) lc in
+  let univ_info = if Array.length lc <= 1 then univ_info
+    else check_univ_leq env_ar_par Univ.Universe.type0 univ_info
+  in
+  let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in
+  (* generalize the constructors over the parameters *)
+  let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in
+  (arity, lc), (indices, splayed_lc), univ_info
+
+(* Allowed eliminations *)
+
+(* Previous comment: *)
+(* Unitary/empty Prop: elimination to all sorts are realizable *)
+(* unless the type is large. If it is large, forbids large elimination *)
+(* which otherwise allows simulating the inconsistent system Type:Type. *)
+(* -> this is now handled by is_smashed: *)
+(* - all_sorts in case of small, unitary Prop (not smashed) *)
+(* - logical_sorts in case of large, unitary Prop (smashed) *)
+
+let all_sorts = [InProp;InSet;InType]
+let small_sorts = [InProp;InSet]
+let logical_sorts = [InProp]
+
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} =
+  if not ind_squashed then all_sorts
+  else match Sorts.family (Sorts.sort_of_univ ind_univ) with
+    | InType -> assert false
+    | InSet -> small_sorts
+    | InProp -> logical_sorts
+
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+   polymorphism. The elements x_k is None if the k-th parameter (starting
+   from the most recent and ignoring let-definitions) is not contributing
+   or is Some u_k if its level is u_k and is contributing. *)
+let param_ccls paramsctxt =
+  let fold acc = function
+    | (LocalAssum (_, p)) ->
+      (let c = Term.strip_prod_assum p in
+      match kind c with
+        | Sort (Type u) -> Univ.Universe.level u
+        | _ -> None) :: acc
+    | LocalDef _ -> acc
+  in
+  List.fold_left fold [] paramsctxt
+
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+  let arity = Vars.subst_univs_level_constr usubst arity in
+  let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
+  let indices = Vars.subst_univs_level_context usubst indices in
+  let splayed_lc = Array.map (fun (args,out) ->
+      let args = Vars.subst_univs_level_context usubst args in
+      let out = Vars.subst_univs_level_constr usubst out in
+      args,out)
+      splayed_lc
+  in
+  let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
+
+  let arity = match univ_info.ind_min_univ with
+    | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+    | Some min_univ ->
+      ((match univs with
+          | Monomorphic_ind _ -> ()
+          | Polymorphic_ind _ | Cumulative_ind _ ->
+            CErrors.anomaly ~label:"polymorphic_template_ind"
+              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
+       TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+  in
+
+  let kelim = allowed_sorts univ_info in
+  (arity,lc), (indices,splayed_lc), kelim
+
+let abstract_inductive_universes = function
+  | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
+  | Polymorphic_ind_entry (nas, ctx) ->
+    let (inst, auctx) = Univ.abstract_universes nas ctx in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Polymorphic_ind auctx)
+  | Cumulative_ind_entry (nas, cumi) ->
+    let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Cumulative_ind acumi)
+
+let typecheck_inductive env (mie:mutual_inductive_entry) =
+  let () = match mie.mind_entry_inds with
+  | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
+  | _ -> ()
+  in
+  (* Check unicity of names (redundant with safe_typing's add_field checks) *)
+  mind_check_names mie;
+  assert (List.is_empty (Environ.rel_context env));
+
+  (* universes *)
+  let env_univs =
+    match mie.mind_entry_universes with
+    | Monomorphic_ind_entry ctx -> push_context_set ctx env
+    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+  in
+
+  (* Params *)
+  let env_params = Typeops.check_context env_univs mie.mind_entry_params in
+  let params = Environ.rel_context env_params in
+
+  (* Arities *)
+  let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in
+  let env_ar_par = push_rel_context params env_ar in
+
+  (* Constructors *)
+  let data = List.map2 (fun ind data -> check_constructors env_ar_par params ind.mind_entry_lc data)
+      mie.mind_entry_inds data
+  in
+
+  let () = match mie.mind_entry_universes with
+    | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data)
+    | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> ()
+  in
+
+  (* Abstract universes *)
+  let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in
+  let params = Vars.subst_univs_level_context usubst params in
+  let data = List.map (abstract_packets univs usubst params) data in
+
+  let env_ar_par =
+    let ctx = Environ.rel_context env_ar_par in
+    let ctx = Vars.subst_univs_level_context usubst ctx in
+    let env = Environ.pop_rel_context (Environ.nb_rel env_ar_par) env_ar_par in
+    Environ.push_rel_context ctx env
+  in
+
+  env_ar_par, univs, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
new file mode 100644
index 0000000000..8841e38636
--- /dev/null
+++ b/kernel/indTyping.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Environ
+open Entries
+open Declarations
+
+(** Type checking for some inductive entry.
+    Returns:
+    - environment with inductives + parameters in rel context
+    - abstracted universes
+    - parameters
+    - for each inductive,
+      (arity * constructors) (with params)
+      * (indices * splayed constructor types) (both without params)
+      * allowed eliminations
+ *)
+val typecheck_inductive : env -> mutual_inductive_entry ->
+  env
+  * abstract_inductive_universes
+  * Constr.rel_context
+  * ((inductive_arity * Constr.types array) *
+     (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
+     Sorts.family list)
+    array
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 68d44f8782..9bb848c6a4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -11,7 +11,6 @@
 open CErrors
 open Util
 open Names
-open Univ
 open Term
 open Constr
 open Vars
@@ -20,9 +19,7 @@ open Declareops
 open Inductive
 open Environ
 open Reduction
-open Typeops
 open Entries
-open Pp
 open Context.Rel.Declaration
 
 (* Terminology:
@@ -49,14 +46,11 @@ let weaker_noccur_between env x nvars t =
    if noccur_between x nvars t' then Some t'
    else None
 
-let is_constructor_head t =
-  isRel(fst(decompose_app t))
-
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
 (* Errors related to inductive constructions *)
-type inductive_error =
+type inductive_error = Type_errors.inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * Id.t * constr * constr * int * int
@@ -67,342 +61,9 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
+  | BadUnivs
 
-exception InductiveError of inductive_error
-
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
-
-let check_constructors_names =
-  let rec check idset = function
-    | [] -> idset
-    | c::cl ->
-	if Id.Set.mem c idset then
-	  raise (InductiveError (SameNamesConstructors c))
-	else
-	  check (Id.Set.add c idset) cl
-  in
-  check
-
-(* [mind_check_names mie] checks the names of an inductive types declaration,
-   and raises the corresponding exceptions when two types or two constructors
-   have the same name. *)
-
-let mind_check_names mie =
-  let rec check indset cstset = function
-    | [] -> ()
-    | ind::inds ->
-	let id = ind.mind_entry_typename in
-	let cl = ind.mind_entry_consnames in
-	if Id.Set.mem id indset then
-	  raise (InductiveError (SameNamesTypes id))
-	else
-	  let cstset' = check_constructors_names cstset cl in
-	  check (Id.Set.add id indset) cstset' inds
-  in
-  check Id.Set.empty Id.Set.empty mie.mind_entry_inds
-(* The above verification is not necessary from the kernel point of
-  vue since inductive and constructors are not referred to by their
-  name, but only by the name of the inductive packet and an index. *)
-
-(************************************************************************)
-(************************************************************************)
-
-(* Typing the arities and constructor types *)
-
-let infos_and_sort env t =
-  let rec aux env t max =
-    let t = whd_all env t in
-      match kind t with
-      | Prod (name,c1,c2) ->
-        let varj = infer_type env c1 in
-	let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in
-        let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in
-	  aux env1 c2 max
-    | _ when is_constructor_head t -> max
-    | _ -> (* don't fail if not positive, it is tested later *) max
-  in aux env t Universe.type0m
-
-(* Computing the levels of polymorphic inductive types
-
-   For each inductive type of a block that is of level u_i, we have
-   the constraints that u_i >= v_i where v_i is the type level of the
-   types of the constructors of this inductive type. Each v_i depends
-   of some of the u_i and of an extra (maybe non variable) universe,
-   say w_i that summarize all the other constraints. Typically, for
-   three inductive types, we could have
-
-   u1,u2,u3,w1 <= u1
-   u1       w2 <= u2
-      u2,u3,w3 <= u3
-
-   From this system of inequations, we shall deduce
-
-   w1,w2,w3 <= u1
-   w1,w2 <= u2
-   w1,w2,w3 <= u3
-*)
-
-(* This (re)computes informations relevant to extraction and the sort of an
-   arity or type constructor; we do not to recompute universes constraints *)
-
-let infer_constructor_packet env_ar_par params lc =
-  (* type-check the constructors *)
-  let jlc = List.map (infer_type env_ar_par) lc in
-  let jlc = Array.of_list jlc in
-  (* generalize the constructor over the parameters *)
-  let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in
-  (* compute the max of the sorts of the products of the constructors types *)
-  let levels = List.map (infos_and_sort env_ar_par) lc in
-  let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
-  let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
-  (lc'', level)
-
-(* If indices matter *)
-let cumulate_arity_large_levels env sign =
-  fst (List.fold_right
-    (fun d (lev,env) ->
-     match d with
-     | LocalAssum (_,t) ->
-	let tj = infer_type env t in
-        let u = Sorts.univ_of_sort tj.utj_type in
-	  (Universe.sup u lev, push_rel d env)
-     | LocalDef _ ->
-	lev, push_rel d env)
-    sign (Universe.type0m,env))
-
-let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
-
-(* Returns the list [x_1, ..., x_n] of levels contributing to template
-   polymorphism. The elements x_k is None if the k-th parameter (starting
-   from the most recent and ignoring let-definitions) is not contributing 
-   or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
-  let fold acc = function
-    | (LocalAssum (_, p)) ->
-      (let c = Term.strip_prod_assum p in
-      match kind c with
-        | Sort (Type u) -> Univ.Universe.level u
-        | _ -> None) :: acc
-    | LocalDef _ -> acc
-  in
-  List.fold_left fold [] paramsctxt
-
-(* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity =
-  let numchecked = ref 0 in
-  let basic_check ev tp =
-    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
-    numchecked := !numchecked + 1
-  in
-  let check_typ typ typ_env =
-    match typ with
-    | LocalAssum (_, typ') ->
-      begin
-       try
-          basic_check typ_env typ'; Environ.push_rel typ typ_env
-        with NotConvertible -> 
-          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
-      end
-    | _ -> anomaly (Pp.str "")
-  in
-  let typs, codom = dest_prod env arcn in
-  let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
-  if not is_arity then basic_check last_env codom else ()
-
-(* 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 numparams = Context.Rel.nhyps paramsctxt in
-    let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx)
-        (fun i -> Level.make (Level.UGlobal.make DirPath.empty i))
-    in
-    let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
-        LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
-    in
-    let dosubst = subst_univs_level_constr lmap in
-    let instance_other = Instance.of_array new_levels in
-    let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
-    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env = Environ.push_context uctx_other env_ar in
-    let subtyp_constraints =
-      CumulativityInfo.leq_constraints cumi
-        (UContext.instance uctx) instance_other
-        Constraint.empty
-    in
-    let env = Environ.add_constraints subtyp_constraints env in
-    (* process individual inductive types: *)
-    Array.iter (fun (_id,_cn,lc,(_sign,arity)) ->
-      match arity with
-        | RegularArity (_, 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
-        | TemplateArity _ ->
-          anomaly ~label:"check_subtyping"
-            Pp.(str "template polymorphism and cumulative polymorphism are not compatible")
-    ) inds
-
-(* Type-check an inductive definition. Does not check positivity
-   conditions. *)
-(* TODO check that we don't overgeneralize construcors/inductive arities with
-   universes that are absent from them. Is it possible? 
-*)
-let typecheck_inductive env mie =
-  let () = match mie.mind_entry_inds with
-  | [] -> anomaly (Pp.str "empty inductive types declaration.")
-  | _ -> ()
-  in
-  (* Check unicity of names *)
-  mind_check_names mie;
-  (* Params are typed-checked here *)
-  let env' =
-    match mie.mind_entry_universes with
-    | Monomorphic_ind_entry ctx -> push_context_set ctx env
-    | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
-    | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
-  in
-  let env_params = check_context env' mie.mind_entry_params in
-  let paramsctxt = mie.mind_entry_params in
-  (* We first type arity of each inductive definition *)
-  (* This allows building the environment of arities and to share *)
-  (* the set of constraints *)
-  let env_arities, rev_arity_list =
-    List.fold_left
-      (fun (env_ar,l) ind ->
-         (* Arities (without params) are typed-checked here *)
-         let template = ind.mind_entry_template in
-         let arity =
-	   if isArity ind.mind_entry_arity then
-	     let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
-	       match s with
-	       | Type u when Univ.universe_level u = None ->
-	         (** We have an algebraic universe as the conclusion of the arity,
-		     typecheck the dummy Π ctx, Prop and do a special case for the conclusion.
-		 *)
-	         let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in
-		 let (cctx, _) = destArity proparity.utj_val in
-		   (* Any universe is well-formed, we don't need to check [s] here *)
-		   mkArity (cctx, s)
-	       | _ -> 
-		 let arity = infer_type env_params ind.mind_entry_arity in
-		   arity.utj_val
-	   else let arity = infer_type env_params ind.mind_entry_arity in
-		  arity.utj_val
-	 in
-	 let (sign, deflev) = dest_arity env_params arity in
-	 let inflev = 
-	   (* The level of the inductive includes levels of indices if 
-	      in indices_matter mode *)
-             if indices_matter env
-	     then Some (cumulate_arity_large_levels env_params sign)
-	     else None
-	 in
-	 (* We do not need to generate the universe of full_arity; if
-	    later, after the validation of the inductive definition,
-	    full_arity is used as argument or subject to cast, an
-	    upper universe will be generated *)
-	 let full_arity = it_mkProd_or_LetIn arity paramsctxt in
-	 let id = ind.mind_entry_typename in
-	 let env_ar' =
-           push_rel (LocalAssum (Name id, full_arity)) env_ar in
-             (* (add_constraints cst2 env_ar) in *)
-           (env_ar', (id,full_arity,sign @ paramsctxt,template,deflev,inflev)::l))
-      (env',[])
-      mie.mind_entry_inds in
-
-  let arity_list = List.rev rev_arity_list in
-
-  (* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
-  let env_ar_par = push_rel_context paramsctxt env_arities in
-
-  (* Now, we type the constructors (without params) *)
-  let inds =
-    List.fold_right2
-      (fun ind arity_data inds ->
-	 let (lc',cstrs_univ) =
-	   infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in
-	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (arity_data,consnames,lc',cstrs_univ) in
-	   ind'::inds)
-      mie.mind_entry_inds
-      arity_list
-    ([]) in
-
-  let inds = Array.of_list inds in
-
-  (* Compute/check the sorts of the inductive types *)
-
-  let inds =
-    Array.map (fun ((id,full_arity,sign,template,def_level,inf_level),cn,lc,clev)  ->
-      let infu = 
-	(** Inferred level, with parameters and constructors. *)
-	match inf_level with
-	| Some alev -> Universe.sup clev alev
-	| None -> clev
-      in
-      let full_polymorphic () = 
-        let defu = Sorts.univ_of_sort def_level in
-	let is_natural =
-	  type_in_type env || (UGraph.check_leq (universes env') infu defu)
-	in
-	let _ =
-	  (** Impredicative sort, always allow *)
-	  if is_impredicative env defu then ()
-	  else (** Predicative case: the inferred level must be lower or equal to the
-		   declared level. *)
-	    if not is_natural then
-	      anomaly ~label:"check_inductive" 
-		(Pp.str"Incorrect universe " ++
-		   Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
-		 ++ Universe.pr infu ++ Pp.str ".")
-	in
-	  RegularArity (not is_natural,full_arity,defu)
-      in
-      let template_polymorphic () =
-        let _sign, s =
-          try dest_arity env full_arity
-          with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
-        in
-        let u = Sorts.univ_of_sort s in
-        (* The polymorphic level is a function of the level of the *)
-        (* conclusions of the parameters *)
-        (* We enforce [u >= lev] in case [lev] has a strict upper *)
-        (* constraints over [u] *)
-        let b = type_in_type env || UGraph.check_leq (universes env') infu u in
-        if not b then
-          anomaly ~label:"check_inductive"
-            (Pp.str"Incorrect universe " ++
-             Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
-             ++ Universe.pr clev ++ Pp.str ".")
-        else
-          TemplateArity (param_ccls paramsctxt, infu)
-      in
-      let arity =
-        match mie.mind_entry_universes with
-        | Monomorphic_ind_entry _ ->
-          if template then template_polymorphic ()
-          else full_polymorphic ()
-        | Polymorphic_ind_entry _ | Cumulative_ind_entry _ ->
-          if template
-          then anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")
-          else full_polymorphic ()
-      in
-	(id,cn,lc,(sign,arity)))
-    inds
-  in
-  (* 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 () = 
-    match mie.mind_entry_universes with
-    | Monomorphic_ind_entry _ -> ()
-    | Polymorphic_ind_entry _ -> ()
-    | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
-  in (env_arities, env_ar_par, paramsctxt, inds)
+exception InductiveError = Type_errors.InductiveError
 
 (************************************************************************)
 (************************************************************************)
@@ -706,21 +367,20 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
     If [chkpos] is [false] then positivity is assumed, and
     [check_positivity_one] computes the subterms occurrences in a
     best-effort fashion. *)
-let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
+let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
   let ntypes = Array.length inds in
   let recursive = finite != BiFinite in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let ra_env_ar = Array.rev_to_list rc in
   let nparamsctxt = Context.Rel.length paramsctxt in
   let nmr = Context.Rel.nhyps paramsctxt in
-  let check_one i (_,lcnames,lc,(sign,_)) =
+  let check_one i (_,lcnames) (nindices,lc) =
     let ra_env_ar_par =
       List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in
     let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in
-    let nnonrecargs = Context.Rel.nhyps sign - nmr in
-    check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc
+    check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nindices lcnames lc
   in
-  let irecargs_nmr = Array.mapi check_one inds in
+  let irecargs_nmr = Array.map2_i check_one names inds in
   let irecargs = Array.map snd irecargs_nmr
   and nmr' = array_min nmr irecargs_nmr
   in (nmr',Rtree.mk_rec irecargs)
@@ -730,48 +390,17 @@ let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds =
 (************************************************************************)
 (* Build the inductive packet *)
 
-(* Allowed eliminations *)
-
-let all_sorts = [InProp;InSet;InType]
-let small_sorts = [InProp;InSet]
-let logical_sorts = [InProp]
-
-let allowed_sorts is_smashed s =
-  if not is_smashed 
-  then (** Naturally in the defined sort.
-	   If [s] is Prop, it must be small and unitary.
-	   Unsmashed, predicative Type and Set: all elimination allowed
-	   as well. *)
-      all_sorts
-  else 
-    match Sorts.family s with
-    (* Type: all elimination allowed: above and below *)
-    | InType -> all_sorts
-    (* Smashed Set is necessarily impredicative: forbids large elimination *)
-    | InSet -> small_sorts
-    (* Smashed to Prop, no informative eliminations allowed *)
-    | InProp -> logical_sorts
-    
-(* Previous comment: *)
-(* Unitary/empty Prop: elimination to all sorts are realizable *)
-(* unless the type is large. If it is large, forbids large elimination *)
-(* which otherwise allows simulating the inconsistent system Type:Type. *)
-(* -> this is now handled by is_smashed: *)
-(* - all_sorts in case of small, unitary Prop (not smashed) *)
-(* - logical_sorts in case of large, unitary Prop (smashed) *)
-
-let arity_conclusion = function
-  | RegularArity (_, c, _) -> c
-  | TemplateArity (_, s) -> mkType s
+let repair_arity indices = function
+  | RegularArity ar -> ar.mind_user_arity
+  | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level)
 
 let fold_inductive_blocks f =
-  Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
-    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign))
+  Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
+    f (Array.fold_left f acc lc) (repair_arity indices arity))
 
 let used_section_variables env inds =
-  let ids = fold_inductive_blocks
-    (fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
-      Id.Set.empty inds in
+  let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
+  let ids = fold_inductive_blocks fold Id.Set.empty inds in
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -842,56 +471,21 @@ let compute_projections (kn, i as ind) mib =
     Array.of_list (List.rev labs),
     Array.of_list (List.rev pbs)
 
-let abstract_inductive_universes iu =
-  match iu with
-  | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
-  | Polymorphic_ind_entry (nas, ctx) ->
-    let (inst, auctx) = Univ.abstract_universes nas ctx in
-    let inst = Univ.make_instance_subst inst in
-    (inst, Polymorphic_ind auctx)
-  | Cumulative_ind_entry (nas, cumi) ->
-    let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
-    let inst = Univ.make_instance_subst inst in
-    (inst, Cumulative_ind acumi)
-
-let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
   let nparamargs = Context.Rel.nhyps paramsctxt in
-  let nparamsctxt = Context.Rel.length paramsctxt in
-  let substunivs, aiu = abstract_inductive_universes iu in
-  let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
-  let env_ar =
-    let ctxunivs = Environ.rel_context env_ar in 
-    let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
-      Environ.push_rel_context ctxunivs' env
-  in
   (* Check one inductive *)
-  let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
+  let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
     (* Type of constructors in normal form *)
-    let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in
-    let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
-    let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
+    let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in
     let consnrealdecls =
-      Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt)
+      Array.map (fun (d,_) -> Context.Rel.length d)
 	splayed_lc in
     let consnrealargs =
-      Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
+      Array.map (fun (d,_) -> Context.Rel.nhyps d)
 	splayed_lc in
-    (* Elimination sorts *)
-    let arkind,kelim = 
-      match ar_kind with
-      | TemplateArity (paramlevs, lev) -> 
-	let ar = {template_param_levels = paramlevs; template_level = lev} in
-	  TemplateArity ar, all_sorts
-      | RegularArity (info,ar,defs) ->
-        let s = Sorts.sort_of_univ defs in
-	let kelim = allowed_sorts info s in
-	let ar = RegularArity 
-	  { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; 
-            mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
-	  ar, kelim in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
@@ -908,10 +502,10 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
     let rtbl = Array.init (List.length cnames) transf in
       (* Build the inductive packet *)
       { mind_typename = id;
-	mind_arity = arkind;
-	mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign;
-	mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
-	mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt;
+        mind_arity = arity;
+        mind_arity_ctxt = indices @ paramsctxt;
+        mind_nrealargs = Context.Rel.nhyps indices;
+        mind_nrealdecls = Context.Rel.length indices;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealdecls;
@@ -923,7 +517,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
       } in
-  let packets = Array.map2 build_one_packet inds recargs in
+  let packets = Array.map3 build_one_packet names inds recargs in
   let mib =
       (* Build the mutual inductive *)
     { mind_record = NotRecord;
@@ -934,7 +528,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
       mind_nparams_rec = nmr;
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
-      mind_universes = aiu;
+      mind_universes = univs;
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
@@ -942,7 +536,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
   let record_info = match isrecord with
   | Some (Some rid) ->
     let is_record pkt =
-      pkt.mind_kelim == all_sorts
+      List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim
       && Array.length pkt.mind_consnames == 1
       && pkt.mind_consnrealargs.(0) > 0
     in
@@ -965,11 +559,17 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in
+  let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
   let chkpos = (Environ.typing_flags env).check_guarded in
-  let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
+  let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
+      mie.mind_entry_inds
+  in
+  let (nmr,recargs) = check_positivity ~chkpos kn names
+      env_ar_par paramsctxt mie.mind_entry_finite
+      (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
+  in
   (* Build the inductive packets *)
-    build_inductive env mie.mind_entry_private mie.mind_entry_universes
-      env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
+    build_inductive env names mie.mind_entry_private univs
+      paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 840e23ed69..7810c1723e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,12 +14,10 @@ open Declarations
 open Environ
 open Entries
 
-(** Inductive type checking and errors *)
-
-(** The different kinds of errors that may result of a malformed inductive
-  definition. *)
+(** Check an inductive. *)
+val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-(** Errors related to inductive constructions *)
+(** Deprecated *)
 type inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
@@ -31,22 +29,8 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
+  | BadUnivs
+[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
 
-exception InductiveError of inductive_error
-
-val infos_and_sort : env -> constr -> Univ.Universe.t
-
-val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit
-
-val check_positivity : chkpos:bool ->
-           Names.MutInd.t ->
-           Environ.env ->
-           (Constr.constr, Constr.types) Context.Rel.pt ->
-           Declarations.recursivity_kind ->
-           ('a * Names.Id.t list * Constr.types array *
-            (('b, 'c) Context.Rel.pt * 'd))
-           array -> Int.t * Declarations.recarg Rtree.t array
-
-(** The following function does checks on inductive declarations. *)
-
-val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
+exception InductiveError of Type_errors.inductive_error
+[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 54c239349d..0b10e788b6 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -39,6 +39,7 @@ Type_errors
 Modops
 Inductive
 Typeops
+IndTyping
 Indtypes
 Cooking
 Term_typing
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 60293fe864..fd050085d7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -68,6 +68,21 @@ type type_error = (constr, types) ptype_error
 
 exception TypeError of env * type_error
 
+type inductive_error =
+  | NonPos of env * constr * constr
+  | NotEnoughArgs of env * constr * constr
+  | NotConstructor of env * Id.t * constr * constr * int * int
+  | NonPar of env * constr * int * constr * constr
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of env * constr
+  | BadEntry
+  | LargeNonPropInductiveNotInType
+  | BadUnivs
+
+exception InductiveError of inductive_error
+
 let nfj env {uj_val=c;uj_type=ct} =
   {uj_val=c;uj_type=nf_betaiota env ct}
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3fd40a7f42..3e954d6a8e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -69,6 +69,25 @@ type type_error = (constr, types) ptype_error
 
 exception TypeError of env * type_error
 
+(** The different kinds of errors that may result of a malformed inductive
+    definition. *)
+type inductive_error =
+  | NonPos of env * constr * constr
+  | NotEnoughArgs of env * constr * constr
+  | NotConstructor of env * Id.t * constr * constr * int * int
+  | NonPar of env * constr * int * constr * constr
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of env * constr
+  | BadEntry
+  | LargeNonPropInductiveNotInType
+  | BadUnivs
+
+exception InductiveError of inductive_error
+
+(** Raising functions *)
+
 val error_unbound_rel : env -> int -> 'a
 
 val error_unbound_var : env -> variable -> 'a