Laxer kernel typing rule for template inductive types.

Under the view that template types are an optimization of sort-polymorphic
inductive types, the requirement that the sort of an argument lives below
the global template universe of the corresponding parameter is spurious.

kernel/inductive.ml

@@ -209,10 +209,59 @@ let subst_univs_sort subs = function
     let fold accu (u, n) = Universe.sup accu (supern u n) in
     Sorts.sort_of_univ (List.fold_left fold (supern u n) rest)
 
-let instantiate_universes ctx (templ, ar) args =
+let get_arity c =
+  let decls, c = Term.decompose_prod_decls c in
+  match kind c with
+  | Sort (Sorts.Type u) ->
+    begin match Universe.level u with
+    | Some l -> (decls, l)
+    | None -> assert false
+    end
+  | _ -> assert false
+
+let rec subst_univs_ctx accu subs ctx params = match ctx, params with
+| [], [] -> accu
+| (LocalDef _ as decl) :: ctx, params ->
+  subst_univs_ctx (decl :: accu) subs ctx params
+| (LocalAssum _ as decl) :: ctx, None :: params ->
+  subst_univs_ctx (decl :: accu) subs ctx params
+| LocalAssum (na, t) :: ctx, Some _ :: params ->
+  let (decls, u) = get_arity t in
+  let u = subst_univs_sort subs (Sorts.sort_of_univ (Universe.make u)) in
+  let decl = LocalAssum (na, Term.it_mkProd_or_LetIn (mkSort u) decls) in
+  subst_univs_ctx (decl :: accu) subs ctx params
+| _, [] | [], _ -> assert false
+
+let instantiate_template_constraints subst templ =
+  let _, cstrs = templ.template_context in
+  let fold (u, cst, v) accu =
+    (* v is not a local universe by the unbounded from below property *)
+    let u = subst_univs_sort subst (Sorts.sort_of_univ (Universe.make u)) in
+    match u with
+    | Sorts.QSort _ | Sorts.SProp -> assert false
+    | Sorts.Prop -> accu
+    | Sorts.Set -> Constraints.add (Univ.Level.set, cst, v) accu
+    | Sorts.Type u ->
+      let fold accu (u, n) = match n, cst with
+      | 0, _ -> Constraints.add (u, cst, v) accu
+      | 1, Le -> Constraints.add (u, Lt, v) accu
+      | 1, (Eq | Lt) -> assert false (* FIXME? *)
+      | _ -> assert false
+      in
+      List.fold_left fold accu (Univ.Universe.repr u)
+  in
+  Constraints.fold fold cstrs Constraints.empty
+
+let instantiate_template_universes (mib, _mip) args =
+  let templ = match mib.mind_template with
+  | None -> assert false
+  | Some t -> t
+  in
+  let ctx = List.rev mib.mind_params_ctxt in
   let subst = make_subst (ctx,templ.template_param_levels,args) in
-  let ty = subst_univs_sort subst ar.template_level in
-  (ctx, ty)
+  let ctx = subst_univs_ctx [] subst ctx templ.template_param_levels in
+  let cstrs = instantiate_template_constraints subst templ in
+  (cstrs, ctx, subst)
 
 (* Type of an inductive type *)
 
@@ -232,51 +281,57 @@ let check_instance mib u =
 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
+  | RegularArity a ->
+    let cst = instantiate_inductive_constraints mib u in
+    subst_instance_constr u a.mind_user_arity, cst
   | TemplateArity ar ->
-    let templ = match mib.mind_template with
-    | None -> assert false
-    | Some t -> t
-    in
-    let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes ctx (templ, 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 *)
-      if not polyprop && not (Sorts.is_prop ar.template_level) && Sorts.is_prop s
-      then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      Term.mkArity (List.rev ctx,s)
+    let cst, params, subst = instantiate_template_universes (mib, mip) paramtyps in
+    let ctx = (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) @ params in
+    let s = subst_univs_sort subst ar.template_level 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 *)
+    if not polyprop && not (Sorts.is_prop ar.template_level) && Sorts.is_prop s
+    then raise (SingletonInductiveBecomesProp mip.mind_typename);
+    Term.mkArity (ctx, s), cst
 
 let type_of_inductive pind =
-  type_of_inductive_gen pind []
+  let (ty, _cst) = type_of_inductive_gen pind [] in
+  ty
 
-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 ((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 constrained_type_of_inductive pind =
+  type_of_inductive_gen pind []
 
 let type_of_inductive_knowing_parameters ?(polyprop=true) mip args =
   type_of_inductive_gen ~polyprop mip args
 
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor (cstr, u) (mib,mip) =
+let type_of_constructor_gen (cstr, u) (mib,mip) paramtyps =
   check_instance mib u;
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
   if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
-  subst_instance_constr u mip.mind_user_lc.(i-1)
-
-let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) =
-  let ty = type_of_constructor cstru ind in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
+  match mip.mind_arity with
+  | RegularArity _ ->
+    let cst = instantiate_inductive_constraints mib u in
+    subst_instance_constr u mip.mind_user_lc.(i-1), cst
+  | TemplateArity _ar ->
+    let cst, params, _ = instantiate_template_universes (mib, mip) paramtyps in
+    let _, typ = Term.decompose_prod_n_decls (List.length mib.mind_params_ctxt) mip.mind_user_lc.(i - 1) in
+    let typ = Term.it_mkProd_or_LetIn typ params in
+    typ, cst
+
+let type_of_constructor pcstr ind =
+  let (ty, _cst) = type_of_constructor_gen pcstr ind [] in
+  ty
+
+let constrained_type_of_constructor cstru ind =
+  type_of_constructor_gen cstru ind []
+
+let type_of_constructor_knowing_parameters cstr specif args =
+  type_of_constructor_gen cstr specif args
 
 let arities_of_constructors (_,u) (_,mip) =
   let map (ctx, c) =

kernel/inductive.mli

@@ -52,9 +52,10 @@ type template_univ =
 
 type param_univs = (expected:Univ.Level.t -> template_univ) list
 
+val instantiate_template_universes : mind_specif -> param_univs ->
+  Constraints.t * rel_context * template_univ Univ.Level.Map.t
+
 val constrained_type_of_inductive : mind_specif puniverses -> types constrained
-val constrained_type_of_inductive_knowing_parameters :
-  mind_specif puniverses -> param_univs -> types constrained
 
 val relevance_of_ind_body : one_inductive_body -> UVars.Instance.t -> Sorts.relevance
 
@@ -63,7 +64,7 @@ val relevance_of_inductive : env -> pinductive -> Sorts.relevance
 val type_of_inductive : mind_specif puniverses -> types
 
 val type_of_inductive_knowing_parameters :
-  ?polyprop:bool -> mind_specif puniverses -> param_univs -> types
+  ?polyprop:bool -> mind_specif puniverses -> param_univs -> types constrained
 
 val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool
 (** For squashing. *)
@@ -81,6 +82,7 @@ val is_primitive_record : mind_specif -> bool
 
 val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
 val type_of_constructor : pconstructor -> mind_specif -> types
+val type_of_constructor_knowing_parameters : pconstructor -> mind_specif -> param_univs -> types constrained
 
 (** Return constructor types in normal form *)
 val arities_of_constructors : pinductive -> mind_specif -> types array

kernel/typeops.ml

@@ -417,11 +417,11 @@ let make_param_univs env indu spec args argtys =
 
 let type_of_inductive_knowing_parameters env (ind,u as indu) args argst =
   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
-      (spec,u) (make_param_univs env indu spec args argst)
-  in
-  check_constraints cst env;
+  let () = assert (Option.has_some mib.mind_template) in
+  let () = check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps in
+  let param_univs = make_param_univs env indu spec args argst in
+  let t, cst = Inductive.type_of_inductive_knowing_parameters (spec,u) param_univs in
+  let () = check_constraints cst env in
   t
 
 let type_of_inductive env (ind,u) =
@@ -433,6 +433,16 @@ let type_of_inductive env (ind,u) =
 
 (* Constructors. *)
 
+let type_of_constructor_knowing_parameters env (c, u as cu) args argst =
+  let ind = inductive_of_constructor c in
+  let (mib, _ as spec) = lookup_mind_specif env ind in
+  let () = assert (Option.has_some mib.mind_template) in
+  let () = check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in
+  let param_univs = make_param_univs env (ind, u) spec args argst in
+  let t, cst = Inductive.type_of_constructor_knowing_parameters cu spec param_univs in
+  let () = check_constraints cst env in
+  t
+
 let type_of_constructor env (c,_u as cu) =
   let (mib, _ as specif) = lookup_mind_specif env (inductive_of_constructor c) in
   let () = check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in
@@ -655,6 +665,8 @@ let rec execute env cstr =
           match kind f with
           | Ind ind when Environ.template_polymorphic_pind ind env ->
             type_of_inductive_knowing_parameters env ind args argst
+          | Construct ((ind, _), _ as cstr) when Environ.template_polymorphic_ind ind env ->
+            type_of_constructor_knowing_parameters env cstr args argst
           | _ ->
             (* No template polymorphism *)
             execute env f
@@ -711,11 +723,19 @@ let rec execute env cstr =
 
         in
         let mib, mip = Inductive.lookup_mind_specif env ci.ci_ind in
-        let cst = Inductive.instantiate_inductive_constraints mib u in
-        let () = check_constraints cst env in
         let pmst = execute_array env pms in
+        let cst, params = match mib.mind_template with
+        | None ->
+          let cst = Inductive.instantiate_inductive_constraints mib u in
+          cst, mib.mind_params_ctxt
+        | Some _ ->
+          let args = make_param_univs env (ci.ci_ind, u) (mib, mip) pms pmst in
+          let (cst, params, _) = instantiate_template_universes (mib, mip) args in
+          cst, params
+        in
+        let () = check_constraints cst env in
         let paramsubst =
-          try type_of_parameters env mib.mind_params_ctxt u pms pmst
+          try type_of_parameters env params u pms pmst
           with ArgumentsMismatch -> error_elim_arity env (ci.ci_ind, u) c None
         in
         let (pctx, pt) =

pretyping/retyping.ml

@@ -217,11 +217,15 @@ let retype ?(polyprop=true) sigma =
       let u = EInstance.kind sigma u in
       let mip = lookup_mind_specif env ind in
       let paramtyps = make_param_univs env sigma (ind,u) args in
-      EConstr.of_constr
-        (Inductive.type_of_inductive_knowing_parameters
-           ~polyprop (mip, u) paramtyps)
+      let (ty, _) = Inductive.type_of_inductive_knowing_parameters ~polyprop (mip, u) paramtyps in
+      EConstr.of_constr ty
     | Construct (cstr, u) ->
-      type_of_constructor env (cstr, u)
+      let u = EInstance.kind sigma u in
+      let (ind, _) = cstr in
+      let mip = lookup_mind_specif env ind in
+      let paramtyps = make_param_univs env sigma (ind, u) args in
+      let (ty, _) = Inductive.type_of_constructor_knowing_parameters (cstr, u) mip paramtyps in
+      EConstr.of_constr ty
     | _ -> assert false
 
   and make_param_univs env sigma indu args =

pretyping/typing.ml

@@ -55,6 +55,13 @@ let inductive_type_knowing_parameters env sigma (ind,u as indu) jl =
   let paramstyp = make_param_univs env sigma indu mspec jl in
   Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
 
+let constructor_type_knowing_parameters env sigma (cstr, u) jl =
+  let u0 = Unsafe.to_instance u in
+  let (ind, _) = cstr in
+  let mspec = lookup_mind_specif env ind in
+  let paramstyp = make_param_univs env sigma (ind, u) mspec jl in
+  Inductive.type_of_constructor_knowing_parameters (cstr, u0) mspec paramstyp
+
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
     | Sort s -> sigma, {utj_val = j.uj_val; utj_type = s }
@@ -111,14 +118,25 @@ let checked_appvect env sigma f args =
 let checked_applist env sigma f args = checked_appvect env sigma f (Array.of_list args)
 
 let judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv =
-  let ar = inductive_type_knowing_parameters env sigma ind argjv in
+  let ar, csts = inductive_type_knowing_parameters env sigma ind argjv in
+  let sigma = Evd.add_constraints sigma csts in
   let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in
   sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
 
 let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
   let (sigma, j) = judge_of_apply env sigma funj argjv in
   judge_of_applied_inductive_knowing_parameters_nocheck env sigma funj ind argjv
 
+let judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj cstr argjv =
+  let ar, csts = constructor_type_knowing_parameters env sigma cstr argjv in
+  let sigma = Evd.add_constraints sigma csts in
+  let typ = hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) in
+  sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
+
+let judge_of_applied_constructor_knowing_parameters env sigma funj ind argjv =
+  let (sigma, j) = judge_of_apply env sigma funj argjv in
+  judge_of_applied_constructor_knowing_parameters_nocheck env sigma funj ind argjv
+
 let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env sigma cj (Array.length explft);
@@ -543,6 +561,9 @@ let rec execute env sigma cstr =
             | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
                let sigma, fj = execute env sigma f in
                judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl
+            | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
+               let sigma, fj = execute env sigma f in
+               judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl
             | _ ->
                (* No template polymorphism *)
                let sigma, fj = execute env sigma f in
@@ -781,6 +802,8 @@ let rec recheck_against env sigma good c =
         (match EConstr.kind sigma f with
          | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
            maybe_changed (judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl)
+         | Construct (cstr, u) when EInstance.is_empty u && Environ.template_polymorphic_ind (fst cstr) env ->
+           maybe_changed (judge_of_applied_constructor_knowing_parameters env sigma fj (cstr, u) jl)
          | _ ->
            (* No template polymorphism *)
            maybe_changed (judge_of_apply env sigma fj jl))