Refactor typechecking of inductive types

We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.

1 files changed, 216 insertions, 274 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8bf34398d7..6976b2019d 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -8,27 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Util
 open Names
 open Univ
 open Term
 open Constr
-open Vars
 open Declarations
 open Environ
-open Reduction
-open Typeops
 open Entries
-open Pp
 open Type_errors
 open Context.Rel.Declaration
 
-let is_constructor_head t =
-  isRel(fst(decompose_app t))
-
-(************************************************************************)
-(* Various well-formedness check for inductive declarations            *)
+(** 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
@@ -67,74 +59,151 @@ let mind_check_names mie =
   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************************)
 (************************************************************************)
 
-(* 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)
+(* 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
@@ -151,215 +220,88 @@ let param_ccls paramsctxt =
   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
+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 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 "")
+  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 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 (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 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
-  | [] -> anomaly (Pp.str "empty inductive types declaration.")
+  | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
   | _ -> ()
   in
-  (* Check unicity of names *)
+  (* Check unicity of names (redundant with safe_typing's add_field checks) *)
   mind_check_names mie;
-  (* Params are typed-checked here *)
-  let env' =
+  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
-  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
+
+  (* 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
-  (* 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)
+
+  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