Removing template polymorphism for definitions.

The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.

Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.

11 files changed, 30 insertions, 165 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 63614e20f..80d41847c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -18,7 +18,6 @@ open Util
 open Names
 open Term
 open Declarations
-open Environ
 open Univ
 
 module NamedDecl = Context.Named.Declaration
@@ -153,7 +152,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
@@ -167,11 +166,6 @@ let on_body ml hy f = function
     OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
-let constr_of_def otab = function
-  | Undef _ -> assert false
-  | Def cs -> Mod_subst.force_constr cs
-  | OpaqueDef lc -> Opaqueproof.force_proof otab lc
-
 let expmod_constr_subst cache modlist subst c =
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
@@ -220,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } =
       List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
       hyps ~init:cb.const_hyps in
-  let typ = match cb.const_type with
-    | RegularArity t ->
-  	let typ =
-          abstract_constant_type (expmod t) hyps in
-  	RegularArity typ
-    | TemplateArity (ctx,s) ->
-  	let t = mkArity (ctx,Type s.template_level) in
-  	let typ = abstract_constant_type (expmod t) hyps in
-  	let j = make_judge (constr_of_def (opaque_tables env) body) typ in
-  	Typeops.make_polymorphic_if_constant_for_ind env j
-  in
+  let typ = abstract_constant_type (expmod cb.const_type) hyps in
   let projection pb =
     let c' = abstract_constant_body (expmod pb.proj_body) hyps in
     let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
@@ -244,9 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
 	  | _ -> assert false 
       with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
     in 
-    let typ = (* By invariant, a regular arity *)
-      match typ with RegularArity t -> t | TemplateArity _ -> assert false 
-    in
     let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_eta = etab, etat;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f386fd936..6d1b776c0 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f35438dfc..9697b0b8b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
-
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
 
@@ -83,7 +81,7 @@ type typing_flags = {
 type constant_body = {
     const_hyps : Context.Named.t; (** New: younger hyp at top *)
     const_body : constant_def;
-    const_type : constant_type;
+    const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
     const_proj : projection_body option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index efce21982..85dd1e66d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -69,10 +69,6 @@ let subst_rel_declaration sub =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-let subst_template_cst_arity sub (ctx,s as arity) =
-  let ctx' = subst_rel_context sub ctx in
-    if ctx==ctx' then arity else (ctx',s)
-      
 let subst_const_type sub arity =
   if is_empty_subst sub then arity
   else subst_mps sub arity
@@ -94,7 +90,7 @@ let subst_const_body sub cb =
   if is_empty_subst sub then cb
   else
     let body' = subst_const_def sub cb.const_body in
-    let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in
+    let type' = subst_const_type sub cb.const_type in
     let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
       && proj' == cb.const_proj then cb
@@ -120,14 +116,6 @@ let hcons_rel_decl =
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
-let hcons_regular_const_arity t = Term.hcons_constr t
-
-let hcons_template_const_arity (ctx, ar) = 
-  (hcons_rel_context ctx, hcons_template_arity ar)
-
-let hcons_const_type = 
-  map_decl_arity hcons_regular_const_arity hcons_template_const_arity
-
 let hcons_const_def = function
   | Undef inl -> Undef inl
   | Def l_constr ->
@@ -145,7 +133,7 @@ let hcons_const_universes cbu =
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
-    const_type = hcons_const_type cb.const_type;
+    const_type = Term.hcons_constr cb.const_type;
     const_universes = hcons_const_universes cb.const_universes }
 
 (** {6 Inductive types } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b01b65200..d2c737ab0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,12 +232,6 @@ let constraints_of cb u =
   | Monomorphic_const _ -> Univ.Constraint.empty
   | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
-let map_regular_arity f = function
-  | RegularArity a as ar -> 
-    let a' = f a in 
-      if a' == a then ar else RegularArity a'
-  | TemplateArity _ -> assert false
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
@@ -245,7 +239,7 @@ let constant_type env (kn,u) =
   | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
   | Polymorphic_const ctx -> 
     let csts = constraints_of cb u in
-    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+    (subst_instance_constr u cb.const_type, csts)
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
@@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) =
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
+	b', subst_instance_constr u cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if Declareops.constant_is_polymorphic cb then
-      map_regular_arity (subst_instance_constr u) cb.const_type
+      subst_instance_constr u cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env =
 let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
-let template_polymorphic_constant cst env =
-  match (lookup_constant cst env).const_type with 
-  | TemplateArity _ -> true
-  | RegularArity _ -> false
-
-let template_polymorphic_pconstant (cst,u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else template_polymorphic_constant cst env
-
 let lookup_projection cst env =
   match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cd7a9d279..377c61de2 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -139,10 +139,6 @@ val polymorphic_constant  : constant -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
 val type_in_type_constant : constant -> env -> bool
 
-(** Old-style polymorphism *)
-val template_polymorphic_constant  : constant -> env -> bool
-val template_polymorphic_pconstant : pconstant -> env -> bool
-
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -153,11 +149,11 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> constant_type constrained
+val constant_type : env -> constant puniverses -> types constrained
 
 val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
 val constant_value_and_type : env -> constant puniverses -> 
-  constr option * constant_type * Univ.constraints
+  constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> constant -> Univ.abstract_universe_context
@@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_universe_context
    already contains the constraints corresponding to the constant 
    application. *)
 val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> constant_type
+val constant_type_in : env -> constant puniverses -> types
 val constant_opt_value_in : env -> constant puniverses -> constr option
 
 (** {6 Primitive projections} *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index c7f3e5c51..0888ccc10 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -83,7 +83,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let c',cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      j.uj_val, cst'
@@ -103,7 +103,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bd82dd465..b311165f1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -313,8 +313,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
           error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let typ1 = cb1.const_type in
+      let typ2 = cb2.const_type in
       let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43c099712..3f42c348f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,7 +21,6 @@ open Environ
 open Entries
 open Typeops
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
@@ -128,7 +127,7 @@ let inline_side_effects env body ctx side_eff =
       match cb.const_universes with
       | Monomorphic_const cnstctx ->
         (** Abstract over the term at the top of the proof *)
-        let ty = Typeops.type_of_constant_type env cb.const_type in
+        let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
         let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
@@ -249,7 +248,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
       {
         Cooking.cook_body = Undef nl;
-        cook_type = RegularArity t;
+        cook_type = t;
         cook_proj = None;
         cook_universes = univs;
         cook_inline = false;
@@ -290,7 +289,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       {
         Cooking.cook_body = def;
-        cook_type = RegularArity typ;
+        cook_type = typ;
         cook_proj = None;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
@@ -320,13 +319,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not poly then (* Old-style polymorphism *)
-             make_polymorphic_if_constant_for_ind env j
-           else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+          Vars.subst_univs_level_constr usubst j.uj_type
         | Some t ->
            let tj = infer_type env t in
            let _ = judge_of_cast env j DEFAULTcast tj in
-           RegularArity (Vars.subst_univs_level_constr usubst t)
+           Vars.subst_univs_level_constr usubst t
       in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
@@ -363,21 +360,13 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
     let term, typ = pb.proj_eta in
     {
       Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
-      cook_type = RegularArity typ;
+      cook_type = typ;
       cook_proj = Some pb;
       cook_universes = univs;
       cook_inline = false;
       cook_context = None;
     }
 
-let global_vars_set_constant_type env = function
-  | RegularArity t -> global_vars_set env t
-  | TemplateArity (ctx,_) ->
-      Context.Rel.fold_outside
-        (RelDecl.fold_constr
-	  (fun t c -> Id.Set.union (global_vars_set env t) c))
-      ctx ~init:Id.Set.empty
-
 let record_aux env s_ty s_bo suggested_expr =
   let in_ty = keep_hyps env s_ty in
   let v =
@@ -426,7 +415,7 @@ let build_constant_declaration kn env result =
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
-        let ids_typ = global_vars_set_constant_type env typ in
+        let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
@@ -454,14 +443,14 @@ let build_constant_declaration kn env result =
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
@@ -524,8 +513,7 @@ let constant_entry_of_side_effect cb u =
     const_entry_body = Future.from_val (pt, ());
     const_entry_secctx = None;
     const_entry_feedback = None;
-    const_entry_type =
-      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -625,7 +613,7 @@ let translate_recipe env kn r =
 let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
-  let typ = type_of_constant_type env decl.cook_type in
+  let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
     match decl.cook_body with
     | Undef _ -> ()
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b814deb6e..044877e82 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign =
 (* Type of constants *)
 
 
-let type_of_constant_type_knowing_parameters env t paramtyps =
-  match t with
-  | RegularArity t -> t
-  | TemplateArity (sign,ar) ->
-      let ctx = List.rev sign in
-      let ctx,s = instantiate_universes env ctx ar paramtyps in
-      mkArity (List.rev ctx,s)
-
-let type_of_constant_knowing_parameters env (kn,u as cst) args =
+let type_of_constant env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   let ty, cu = constant_type env cst in
-  let ty = type_of_constant_type_knowing_parameters env ty args in
   let () = check_constraints cu env in
     ty
 
-let type_of_constant_knowing_parameters_in env (kn,u as cst) args =
+let type_of_constant_in env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
-  let ty = constant_type_in env cst in
-  type_of_constant_type_knowing_parameters env ty args
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
-  type_of_constant_knowing_parameters_in env cst [||]
-
-let type_of_constant_type env t =
-  type_of_constant_type_knowing_parameters env t [||]
+  constant_type_in env cst
 
 (* Type of a lambda-abstraction. *)
 
@@ -369,9 +350,6 @@ let rec execute env cstr =
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_inductive_knowing_parameters env ind args
-	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
-	    let args = Array.map (fun t -> lazy t) argst in
-              type_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* No template polymorphism *)
             execute env f
@@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
 let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
 
 let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst)
-let judge_of_constant_knowing_parameters env cst args =
-  make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args)
 
 let judge_of_projection env p cj =
   make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type)
@@ -559,34 +535,3 @@ let type_of_projection_constant env (p,u) =
       Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-(* Instantiation of terms on real arguments. *)
-
-(* Make a type polymorphic if an arity *)
-
-let extract_level env p =
-  let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
-
-let extract_context_levels env l =
-  let fold l = function
-    | RelDecl.LocalAssum (_,p) -> extract_level env p :: l
-    | RelDecl.LocalDef _ -> l
-  in
-  List.fold_left fold [] l
-
-let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
-  let params, ccl = dest_prod_assum env t in
-  match kind_of_term ccl with
-  | Sort (Type u) ->
-     let ind, l = decompose_app (whd_all env c) in
-     if isInd ind && List.is_empty l then
-       let mis = lookup_mind_specif env (fst (destInd ind)) in
-       let nparams = Inductive.inductive_params mis in
-       let paramsl = CList.lastn nparams params in
-       let param_ccls = extract_context_levels env paramsl in
-       let s = { template_param_levels = param_ccls; template_level = u} in
-       TemplateArity (params,s)
-     else RegularArity t
-  | _ ->
-      RegularArity t
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 24521070e..a8f7fba9a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -11,7 +11,6 @@ open Univ
 open Term
 open Environ
 open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
 
@@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 
 val judge_of_constant : env -> pconstant -> unsafe_judgment
 
-val judge_of_constant_knowing_parameters :
-  env -> pconstant -> types Lazy.t array -> unsafe_judgment
-
 (** {6 type of an applied projection } *)
 
 val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
@@ -98,21 +94,9 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_constant_type : env -> constant_type -> types
-
 val type_of_projection_constant : env -> Names.projection puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types
 
-val type_of_constant_type_knowing_parameters :
-  env -> constant_type -> types Lazy.t array -> types
-
-val type_of_constant_knowing_parameters_in :
-  env -> pconstant -> types Lazy.t array -> types
-
-(** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
-  constant_type
-
 (** Check that hyps are included in env and fails with error otherwise *)
 val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit