Add explicit atribute for template polymorphism.

9 files changed, 99 insertions, 35 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5fc4293cbb..bbc0a37c69 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1499,7 +1499,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
new file mode 100644
index 0000000000..a8fe1baa1b
--- /dev/null
+++ b/test-suite/success/Template.v
@@ -0,0 +1,36 @@
+Set Printing Universes.
+
+Module Auto.
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  (* This checks that Box is template poly, see module No for how it fails *)
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End Auto.
+
+Module Yes.
+  #[template]
+  Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End Yes.
+
+Module No.
+  #[notemplate]
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Fail Definition box_lti A := Box A : Type@{i}.
+End No.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d23784f774..7745f3eec7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -336,7 +336,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations cum poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   if not (List.is_empty uparamsl) && not (List.is_empty notations)
@@ -420,13 +420,21 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
     constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> {
-    mind_entry_typename = ind.ind_name;
-    mind_entry_arity = arity;
-    mind_entry_template = not poly && Option.cata (fun s -> not (Sorts.is_small s)) false concl;
-    mind_entry_consnames = cnames;
-    mind_entry_lc = ctypes
-  }) indl arities arityconcl constructors in
+  let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+      let template = match template with
+        | Some template ->
+          if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+          template
+        | None -> not poly && Option.cata (fun s -> not (Sorts.is_small s)) false concl
+      in
+      { mind_entry_typename = ind.ind_name;
+        mind_entry_arity = arity;
+        mind_entry_template = template;
+        mind_entry_consnames = cnames;
+        mind_entry_lc = ctypes
+      })
+      indl arities arityconcl constructors
+  in
   let impls =
     let len = Context.Rel.nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
@@ -456,8 +464,8 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
-  interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ~template ([],paramsl,indl) notations cum poly prv finite
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -545,11 +553,11 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template indl cum poly prv ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template indl ntns cum poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 4e30ed7de5..b523e9c014 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,7 +24,7 @@ type uniform_inductive_flag =
   | NonUniformParameters
 
 val do_mutual_inductive :
-  (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+  template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
   Declarations.recursivity_kind -> unit
 
@@ -67,6 +67,6 @@ val extract_mutual_inductive_declaration_components :
 (** Typing mutual inductive definitions *)
 
 val interp_mutual_inductive :
-  structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+  template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/record.ml b/vernac/record.ml
index af4fd0846c..3e88489208 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -393,14 +393,14 @@ open Typeclasses
 
 let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
   let nparams = List.length params in
-  let template, ctx =
+  let poly, ctx =
     match univs with
     | Monomorphic_ind_entry ctx ->
-      template, Monomorphic_const_entry Univ.ContextSet.empty
+      false, Monomorphic_const_entry Univ.ContextSet.empty
     | Polymorphic_ind_entry ctx ->
-      false, Polymorphic_const_entry ctx
+      true, Polymorphic_const_entry ctx
     | Cumulative_ind_entry cumi ->
-      false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+      true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name =
     match name with
@@ -418,9 +418,16 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
     let type_constructor = it_mkProd_or_LetIn ind fields in
     let template =
-      template &&
-      let _, s = Reduction.dest_arity (Global.env()) arity in
-      not (Sorts.is_small s)
+      match template with
+      | Some template, _ ->
+        (* templateness explicitly requested *)
+        if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+        template
+      | None, template ->
+        (* auto detect template *)
+        template && not poly &&
+        let _, s = Reduction.dest_arity (Global.env()) arity in
+        not (Sorts.is_small s)
     in
     { mind_entry_typename = id;
       mind_entry_arity = arity;
@@ -446,7 +453,6 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
     let build = ConstructRef cstr in
-    let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
     let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
     rsp
@@ -661,13 +667,14 @@ let extract_record_data records =
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions
    or subinstances. *)
-let definition_structure kind cum poly finite records =
+let definition_structure kind ~template cum poly finite records =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let pl, ps, data = extract_record_data records in
-  let pl, univs, template, params, implpars, data =
+  let pl, univs, auto_template, params, implpars, data =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+        typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+  let template = template, auto_template in
   match kind with
   | Class def ->
     let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
diff --git a/vernac/record.mli b/vernac/record.mli
index 567f2b3138..055a17895a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,8 @@ val declare_projections :
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :
-  inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+  inductive_kind -> template:bool option ->
+  Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
   Declarations.recursivity_kind ->
   (coercion_flag *
   Names.lident *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 681dce3ca3..e6b3721134 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -555,7 +555,7 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record cum k poly finite records =
+let vernac_record ~template cum k poly finite records =
   let is_cumulative = should_treat_as_cumulative cum poly in
   let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
     let const = match nameopt with
@@ -577,7 +577,7 @@ let vernac_record cum k poly finite records =
     coe, id, pl, binders, cfs, const, sort
   in
   let records = List.map map records in
-  ignore(Record.definition_structure k is_cumulative poly finite records)
+  ignore(Record.definition_structure ~template k is_cumulative poly finite records)
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
@@ -606,13 +606,14 @@ let vernac_inductive ~atts cum lo finite indl =
   | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
   | _ -> None
   in
+  let template = atts.template in
   if Option.has_some is_defclass then
     (** Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
-    vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+    vernac_record ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (** Mutual record case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -635,7 +636,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record cum kind atts.polymorphic finite recordl
+    vernac_record ~template cum kind atts.polymorphic finite recordl
   else if List.for_all is_constructor indl then
     (** Mutual inductive case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -661,7 +662,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template indl is_cumulative atts.polymorphic lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
@@ -2358,6 +2359,14 @@ let attributes_of_flags f atts =
          (Some false, atts)
        | ("polymorphic" | "monomorphic") ->
          user_err Pp.(str "Polymorphism specified twice")
+       | "template" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some true }
+       | "notemplate" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some false }
+       | "template" | "notemplate" ->
+         user_err Pp.(str "Templateness specified twice")
        | "local" when Option.is_empty atts.locality ->
          assert_empty k v;
          (polymorphism, { atts with locality = Some true })
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1bb1414f3d..2746cbd144 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,12 +21,13 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  template : bool option;
   program : bool;
   deprecated : deprecation option;
 }
 
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
-  { loc ; locality ; polymorphic ; program ; deprecated }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
+  { loc ; locality ; polymorphic ; program ; deprecated; template }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 46468b3098..62a178b555 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -18,12 +18,14 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  template : bool option;
   program : bool;
   deprecated : deprecation option;
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+  ?polymorphic: bool -> ?template:bool option ->
+  ?program: bool -> ?deprecated: deprecation option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t