Use thunks to univ instead of lazy constr for template typing

16 files changed, 81 insertions, 55 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3771454db5..b6b8e5265c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let auxntyp = 1 in
   let specif = (lookup_mind_specif env mi, u) in
-  let ty = type_of_inductive env specif in
+  let ty = type_of_inductive specif in
   let env' =
     let r = (snd (fst specif)).mind_relevance in
     let anon = Context.make_annot Anonymous r in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5d8e1f0fdb..c6035f78ff 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -143,9 +143,16 @@ let remember_subst u subst =
     Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
   with Not_found -> subst
 
+type param_univs = (unit -> Universe.t) list
+
+let make_param_univs env argtys =
+  Array.map_to_list (fun arg () ->
+      Sorts.univ_of_sort (snd (Reduction.dest_arity env arg)))
+    argtys
+
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let make_subst env =
+let make_subst =
   let rec make subst = function
     | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
@@ -158,8 +165,8 @@ let make_subst env =
         (* arity is a global level which, at typing time, will be enforce *)
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
-        let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in
-          make (cons_subst u s subst) (sign, exp, args)
+        let s = a () in
+        make (cons_subst u s subst) (sign, exp, args)
     | LocalAssum (_na,_t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
@@ -178,9 +185,8 @@ let make_subst env =
 
 exception SingletonInductiveBecomesProp of Id.t
 
-let instantiate_universes env ctx ar argsorts =
-  let args = Array.to_list argsorts in
-  let subst = make_subst env (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx ar args =
+  let subst = make_subst (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -204,13 +210,13 @@ let check_instance mib u =
       | Polymorphic uctx -> Instance.length u = AUContext.size uctx)
   then CErrors.anomaly Pp.(str "bad instance length on mutind.")
 
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
   check_instance mib u;
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes env ctx ar paramtyps in
+    let ctx,s = instantiate_universes ctx ar paramtyps in
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
@@ -218,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       Term.mkArity (List.rev ctx,s)
 
-let type_of_inductive env pind =
-  type_of_inductive_gen env pind [||]
+let type_of_inductive pind =
+  type_of_inductive_gen pind []
 
-let constrained_type_of_inductive env ((mib,_mip),u as pind) =
-  let ty = type_of_inductive env pind in
+let constrained_type_of_inductive ((mib,_mip),u as pind) =
+  let ty = type_of_inductive pind in
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args =
-  let ty = type_of_inductive_gen env pind args in
+let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args =
+  let ty = type_of_inductive_gen pind args in
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
-  type_of_inductive_gen ~polyprop env mip args
+let type_of_inductive_knowing_parameters ?(polyprop=true) mip args =
+  type_of_inductive_gen ~polyprop mip args
 
 (* The max of an array of universes *)
 
@@ -589,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let push_ind specif env =
     let r = specif.mind_relevance in
     let anon = Context.make_annot Anonymous r in
-    let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+    let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in
     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8c40c318c5..b690fe1157 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex
 val instantiate_inductive_constraints :
   mutual_inductive_body -> Instance.t -> Constraint.t
 
-val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
+type param_univs = (unit -> Universe.t) list
+
+val make_param_univs : Environ.env -> constr array -> param_univs
+(** The constr array is the types of the arguments to a template
+    polymorphic inductive. *)
+
+val constrained_type_of_inductive : mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters :
-  env -> mind_specif puniverses -> types Lazy.t array -> types constrained
+  mind_specif puniverses -> param_univs -> types constrained
 
 val relevance_of_inductive : env -> inductive -> Sorts.relevance
 
-val type_of_inductive : env -> mind_specif puniverses -> types
+val type_of_inductive : mind_specif puniverses -> types
 
 val type_of_inductive_knowing_parameters :
-  env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
+  ?polyprop:bool -> mind_specif puniverses -> param_univs -> types
 
 val elim_sort : mind_specif -> Sorts.family
 
@@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : Sorts.t array -> Universe.t
 
-val instantiate_universes : env -> Constr.rel_context ->
-  template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t
+val instantiate_universes : Constr.rel_context ->
+  template_arity -> param_univs -> Constr.rel_context * Sorts.t
 
 (** {6 Debug} *)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0a654adf7f..11c455de73 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let ty1 = type_of_inductive env ((mib1, p1), inst) in
-      let ty2 = type_of_inductive env ((mib2, p2), inst) in
+      let ty1 = type_of_inductive ((mib1, p1), inst) in
+      let ty2 = type_of_inductive ((mib2, p2), inst) in
       let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
         cst
   in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2a35f87db8..80accc1ced 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -372,7 +372,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args =
   let (mib,_mip) as spec = lookup_mind_specif env ind in
   check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
   let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
-    env (spec,u) args
+      (spec,u) (Inductive.make_param_univs env args)
   in
   check_constraints cst env;
   t
@@ -380,7 +380,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args =
 let type_of_inductive env (ind,u) =
   let (mib,mip) = lookup_mind_specif env ind in
   check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
-  let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
+  let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in
   check_constraints cst env;
   t
 
@@ -461,8 +461,7 @@ let type_of_global_in_context env r =
     let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
     let univs = Declareops.inductive_polymorphic_context mib in
     let inst = Univ.make_abstract_instance univs in
-    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
-    Inductive.type_of_inductive env (specif, inst), univs
+    Inductive.type_of_inductive (specif, inst), univs
   | ConstructRef cstr ->
     let (mib,_ as specif) =
       Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
@@ -515,8 +514,7 @@ let rec execute env cstr =
         let f', ft =
           match kind f with
           | Ind ind when Environ.template_polymorphic_pind ind env ->
-            let args = Array.map (fun t -> lazy t) argst in
-              f, type_of_inductive_knowing_parameters env ind args
+            f, type_of_inductive_knowing_parameters env ind argst
           | _ ->
             (* No template polymorphism *)
             execute env f
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a4469b7ec1..9b30ddd958 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -437,7 +437,7 @@ and extract_really_ind env kn mib =
       Array.mapi
         (fun i mip ->
            let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in
-           let ar = Inductive.type_of_inductive env ((mib,mip),u) in
+           let ar = Inductive.type_of_inductive ((mib,mip),u) in
            let ar = EConstr.of_constr ar in
            let info = (fst (flag_of_type env sg ar) = Info) in
            let s,v = if info then type_sign_vl env sg ar else [],[] in
@@ -526,7 +526,7 @@ and extract_really_ind env kn mib =
         (* Is this record officially declared with its projections ? *)
         (* If so, we use this information. *)
         begin try
-          let ty = Inductive.type_of_inductive env ((mib,mip0),u) in
+          let ty = Inductive.type_of_inductive ((mib,mip0),u) in
           let n = nb_default_params env sg (EConstr.of_constr ty) in
           let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
           in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 816a8c4703..a4406aeba1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -29,7 +29,7 @@ open Context.Rel.Declaration
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
  Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
- Inductive.type_of_inductive env (specif,u)
+ Inductive.type_of_inductive (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bfee07e7f0..838bf22c66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1707,7 +1707,7 @@ let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match EConstr.kind sigma c with
     | Sort s -> l,s
-    | _ -> invalid_arg "splay_arity"
+    | _ -> raise Reduction.NotArity
 
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e72f5f2793..c539ec55ed 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -236,12 +236,20 @@ val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
+val splay_prod_assum : env ->  evar_map -> constr -> rel_context * constr
+
 val splay_arity : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val sort_of_arity : env -> evar_map -> constr -> ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
-val splay_prod_assum :
-  env ->  evar_map -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d2af957b54..87fe4cfcda 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma =
     | _ -> decomp_sort env sigma (type_of env t)
 
   and type_of_global_reference_knowing_parameters env c args =
-    let argtyps =
-      Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
     match EConstr.kind sigma c with
     | Ind (ind, u) ->
       let u = EInstance.kind sigma u in
       let mip = lookup_mind_specif env ind in
-        EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
-               ~polyprop env (mip, u) argtyps
-         with Reduction.NotArity -> retype_error NotAnArity)
+      let paramtyps = Array.map_to_list (fun arg () ->
+          let t = type_of env arg in
+          let s = try Reductionops.sort_of_arity env sigma t
+            with Reduction.NotArity -> retype_error NotAnArity
+          in
+          Sorts.univ_of_sort (ESorts.kind sigma s))
+          args
+      in
+      EConstr.of_constr
+        (Inductive.type_of_inductive_knowing_parameters
+           ~polyprop (mip, u) paramtyps)
     | Construct (cstr, u) ->
       let u = EInstance.kind sigma u in
       EConstr.of_constr (type_of_constructor env (cstr, u))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b4c19775a7..f067c075bf 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -38,8 +38,11 @@ let meta_type evd mv =
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
-  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
-  Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+  let paramstyp = Array.map_to_list (fun j () ->
+      let s = Reductionops.sort_of_arity env sigma j.uj_type in
+      Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl
+  in
+  Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) =
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
   let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
-  let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+  let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in
   let sigma = Evd.add_constraints sigma csts in
   sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 885fc8980d..b04e59734d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ =
 let construct_of_constr_block = construct_of_constr false
 
 let type_of_ind env (ind, u) =
-  type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
+  type_of_inductive (Inductive.lookup_mind_specif env ind, u)
 
 let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
   let rtbl = mip.mind_reloc_tbl in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index a5fd7f69ed..b84113bde2 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -85,8 +85,8 @@ let print_constructors envpar sigma names types =
   in
   hv 0 (str "  " ++ pc)
 
-let build_ind_type env mip =
-  Inductive.type_of_inductive env mip
+let build_ind_type mip =
+  Inductive.type_of_inductive mip
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
@@ -94,7 +94,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let params = Inductive.inductive_paramdecls (mib,u) in
   let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
   let envpar = push_rel_context params env in
@@ -146,7 +146,7 @@ let print_record env mind mib udecl =
   let params = Inductive.inductive_paramdecls (mib,u) in
   let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index fb61a1089f..46f616c4ff 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -239,7 +239,6 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
      in
      (* Build the context of all arities *)
      let arities_ctx =
-       let global_env = Global.env () in
        let instance =
          let open Univ in
          Instance.of_array
@@ -250,7 +249,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
        in
        Array.fold_left (fun accu oib ->
           let pspecif = ((mib, oib), instance) in
-          let ind_type = Inductive.type_of_inductive global_env pspecif in
+          let ind_type = Inductive.type_of_inductive pspecif in
           let indr = oib.mind_relevance in
           let ind_name = Name oib.mind_typename in
           Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 6bdb3159cf..bdf8511cce 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -178,7 +178,7 @@ let build_beq_scheme mode kn =
   (* current inductive we are working on *)
   let cur_packet = mib.mind_packets.(snd (fst ind)) in
   (* Inductive toto : [rettyp] := *)
-  let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in
+  let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in
   (* split rettyp in a list without the non rec params and the last ->
   e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
   let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
diff --git a/vernac/record.ml b/vernac/record.ml
index 27bd390714..3e44cd85cc 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -622,7 +622,7 @@ let add_inductive_class env sigma ind =
     let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
     let env = push_rel_context ctx env in
     let inst = Univ.make_abstract_instance univs in
-    let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+    let ty = Inductive.type_of_inductive ((mind, oneind), inst) in
     let r = Inductive.relevance_of_inductive env ind in
       { cl_univs = univs;
         cl_impl = GlobRef.IndRef ind;