Fix #7754: universe declarations on mutual inductives

8 files changed, 75 insertions, 44 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bbc0a37c69..fd2d90e9cf 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1469,7 +1469,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    (((CAst.make @@ relnames.(i)), None),
+    ((CAst.make @@ relnames.(i)),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
@@ -1499,14 +1499,14 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds =
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg =
@@ -1521,7 +1521,7 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds =
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg =
diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v
new file mode 100644
index 0000000000..229df93773
--- /dev/null
+++ b/test-suite/bugs/closed/7754.v
@@ -0,0 +1,21 @@
+
+Set Universe Polymorphism.
+
+Module OK.
+
+  Inductive one@{i j} : Type@{i} :=
+  with two : Type@{j} := .
+  Check one@{Set Type} : Set.
+  Fail Check two@{Set Type} : Set.
+
+End OK.
+
+Module Bad.
+
+  Fail Inductive one :=
+    with two@{i +} : Type@{i} := .
+
+  Fail Inductive one@{i +} :=
+    with two@{i +} := .
+
+End Bad.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index fb9d21c429..7b28895814 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -67,7 +67,6 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -348,13 +347,12 @@ 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 ~template (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template udecl (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)
   then user_err (str "Inductives with uniform parameters may not have attached notations.");
-  let pl = (List.hd indl).ind_univs in
-  let sigma, decl = interp_univ_decl_opt env0 pl in
+  let sigma, udecl = interp_univ_decl_opt env0 udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
     interp_context_evars env0 sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -424,7 +422,7 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
   let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
-  let uctx = Evd.check_univ_decl ~poly sigma decl in
+  let uctx = Evd.check_univ_decl ~poly sigma udecl in
   List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
   Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -478,8 +476,8 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-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
+let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -500,8 +498,8 @@ let extract_params indl =
       params
 
 let extract_inductive indl =
-  List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
-    ind_name = indname; ind_univs = pl;
+  List.map (fun ({CAst.v=indname},_,ar,lc) -> {
+    ind_name = indname;
     ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
     ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
   }) indl
@@ -567,11 +565,11 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive ~template indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template udecl 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()) ~template indl ntns cum poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl 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 8a2c9b8719..f23085a538 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,7 +24,8 @@ type uniform_inductive_flag =
   | NonUniformParameters
 
 val do_mutual_inductive :
-  template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+  template:bool option -> universe_decl_expr option ->
+  (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
   Declarations.recursivity_kind -> unit
 
@@ -54,7 +55,6 @@ val should_auto_template : unit -> bool
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
-  ind_univs : universe_decl_expr option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -69,6 +69,7 @@ val extract_mutual_inductive_declaration_components :
 (** Typing mutual inductive definitions *)
 
 val interp_mutual_inductive :
-  template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+  template:bool option -> universe_decl_expr 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 7ab2b50764..724b6e62fe 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -628,7 +628,7 @@ let check_unique_names records =
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
     | _ -> acc in
   let allnames =
-    List.fold_left (fun acc (_, id, _, _, cfs, _, _) ->
+    List.fold_left (fun acc (_, id, _, cfs, _, _) ->
       id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
   in
   match List.duplicates Id.equal allnames with
@@ -637,19 +637,19 @@ let check_unique_names records =
 
 let check_priorities kind records =
   let isnot_class = match kind with Class false -> false | _ -> true in
-  let has_priority (_, _, _, _, cfs, _, _) =
+  let has_priority (_, _, _, cfs, _, _) =
     List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
   in
   if isnot_class && List.exists has_priority records then
     user_err Pp.(str "Priorities only allowed for type class substructures")
 
 let extract_record_data records =
-  let map (is_coe, id, _, _, cfs, idbuild, s) =
+  let map (is_coe, id, _, cfs, idbuild, s) =
     let fs = List.map (fun (((_, f), _), _) -> f) cfs in
     id.CAst.v, s, List.map snd cfs, fs
   in
   let data = List.map map records in
-  let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in
+  let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
   let ps = match pss with
   | [] -> CErrors.anomaly (str "Empty record block")
   | ps :: rem ->
@@ -661,30 +661,28 @@ let extract_record_data records =
     in
     ps
   in
-  (** FIXME: Same issue as #7754 *)
-  let _, _, pl, _, _, _, _ = List.hd records in
-  pl, ps, data
+  ps, data
 
 (* [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 ~template cum poly finite records =
+let definition_structure udecl 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, auto_template, params, implpars, data =
+  let ps, data = extract_record_data records in
+  let ubinders, 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 udecl 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
+    let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
     let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
     let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
-    declare_class finite def cum pl univs id.CAst.v idbuild
+    declare_class finite def cum ubinders univs id.CAst.v idbuild
       implpars params arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
@@ -699,11 +697,11 @@ let definition_structure kind ~template cum poly finite records =
         | Monomorphic_const_entry univs ->
           Monomorphic_ind_entry univs
       in
-    let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) =
+    let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
       let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
-    let inds = declare_structure finite pl univs implpars params template data in
+    let inds = declare_structure finite ubinders univs implpars params template data in
     List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 055a17895a..953d5ec3b6 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,12 +26,11 @@ val declare_projections :
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :
-  inductive_kind -> template:bool option ->
+  universe_decl_expr option -> inductive_kind -> template:bool option ->
   Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
   Declarations.recursivity_kind ->
   (coercion_flag *
   Names.lident *
-  universe_decl_expr option *
   local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option) list ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 28abd1e6ef..015d5fabef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -555,9 +555,9 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record ~template cum k poly finite records =
+let vernac_record ~template udecl 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 map ((coe, id), binders, sort, nameopt, cfs) =
     let const = match nameopt with
     | None -> add_prefix "Build_" id.v
     | Some lid ->
@@ -574,10 +574,22 @@ let vernac_record ~template cum k poly finite records =
         in
         List.iter iter cfs
     in
-    coe, id, pl, binders, cfs, const, sort
+    coe, id, binders, cfs, const, sort
   in
   let records = List.map map records in
-  ignore(Record.definition_structure ~template k is_cumulative poly finite records)
+  ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records)
+
+let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
+  match indl with
+  | [] -> assert false
+  | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
+    let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+        if Option.has_some udecl
+        then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
+        else (((coe,id),b,c,k,d),e))
+        rest
+    in
+    udecl, (((coe,id),b,c,k,d),e) :: rest
 
 (** 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]
@@ -585,8 +597,9 @@ let vernac_record ~template cum k poly finite records =
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
   let open Pp in
+  let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
-    List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
+    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with
 	| Constructors cstrs ->
 	    Dumpglob.dump_definition lid false "ind";
@@ -594,6 +607,7 @@ let vernac_inductive ~atts cum lo finite indl =
 			 Dumpglob.dump_definition lid false "constr") cstrs
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
+
   let is_record = function
   | ((_ , _ , _ , _, RecordDecl _), _) -> true
   | _ -> false
@@ -613,7 +627,7 @@ let vernac_inductive ~atts cum lo finite indl =
     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 ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+    vernac_record ~template udecl 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
@@ -636,7 +650,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 ~template cum kind atts.polymorphic finite recordl
+    vernac_record ~template udecl 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
@@ -662,7 +676,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 ~template indl is_cumulative atts.polymorphic lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ea69ed59a3..0c0204a728 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -202,7 +202,7 @@ type inductive_expr =
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
+  lident * local_binder_expr list * constr_expr option * constructor_expr list
 
 type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list