Pass around information on the use of template polymorphism for

inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).

9 files changed, 45 insertions, 32 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index f6958849b0..baeec31b4b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -37,6 +37,7 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
   mind_entry_arity : constr;
+  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_consnames : Id.t list;
   mind_entry_lc : constr list }
 
@@ -48,7 +49,7 @@ type mutual_inductive_entry = {
   mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
-  mind_entry_polymorphic : bool;
+  mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
   mind_entry_private : bool option }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index afd7cde979..6dd3ab2ba9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -226,7 +226,8 @@ let typecheck_inductive env ctx mie =
     List.fold_left
       (fun (env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-         let arity, expltype = 
+	 let expltype = ind.mind_entry_template in
+         let arity =
 	   if isArity ind.mind_entry_arity then
 	     let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
 	       match s with
@@ -237,12 +238,12 @@ let typecheck_inductive env ctx mie =
 	         let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
 		 let (cctx, _) = destArity proparity.utj_val in
 		   (* Any universe is well-formed, we don't need to check [s] here *)
-		   mkArity (cctx, s), not (Sorts.is_small s)
+		   mkArity (cctx, s)
 	       | _ -> 
 		 let arity = infer_type env_params ind.mind_entry_arity in
-		   arity.utj_val, not (Sorts.is_small s)
+		   arity.utj_val
 	   else let arity = infer_type env_params ind.mind_entry_arity in
-		  arity.utj_val, false
+		  arity.utj_val
 	 in
 	 let (sign, deflev) = dest_arity env_params arity in
 	 let inflev = 
diff --git a/library/declare.ml b/library/declare.ml
index fb6e1c9b81..56c789c1ed 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -353,6 +353,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
   mind_entry_arity = mkProp;
+  mind_entry_template = false;
   mind_entry_consnames = mie.mind_entry_consnames;
   mind_entry_lc = []
 }
diff --git a/library/universes.ml b/library/universes.ml
index 438e6cc532..d69386ddf9 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -957,10 +957,13 @@ let is_direct_sort_constraint s v = match s with
 let solve_constraints_system levels level_bounds level_min =
   let open Univ in
   let levels =
-    Array.map (Option.map
-		 (fun u -> match Universe.level u with 
-		 | Some u -> u 
-		 | _ -> Errors.anomaly (Pp.str"expects Atom")))
+    Array.mapi (fun i o ->
+      match o with
+      | Some u ->
+	(match Universe.level u with 
+	| Some u -> Some u 
+	| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+      | None -> None)
       levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
new file mode 100644
index 0000000000..8da4f73626
--- /dev/null
+++ b/test-suite/bugs/closed/3821.v
@@ -0,0 +1,2 @@
+Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
+
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f8c9f25b89..cd5aa7528e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -529,12 +529,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
+  let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
     mind_entry_typename = ind.ind_name;
     mind_entry_arity = arity;
+    mind_entry_template = template;
     mind_entry_consnames = cnames;
     mind_entry_lc = ctypes
-  }) indl arities constructors in
+  }) indl arities aritypoly constructors in
   let impls =
     let len = rel_context_nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 1823e3a89a..7a79b2efb8 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -43,26 +43,27 @@ let abstract_inductive hyps nparams inds =
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
     List.map
-      (function (tname,arity,cnames,lc) ->
+      (function (tname,arity,template,cnames,lc) ->
 	let lc' = List.map (substl subs) lc in
 	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
 	let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
-        (tname,arity',cnames,lc''))
+        (tname,arity',template,cnames,lc''))
       	inds in
   let nparams' = nparams + Array.length args in
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
-  let params' = let (_,arity,_,_) = List.hd inds' in
+  let params' = let (_,arity,_,_,_) = List.hd inds' in
 		let (params,_) = decompose_prod_n_assum nparams' arity in
 		  List.map detype_param params
   in
   let ind'' =
   List.map
-    (fun (a,arity,c,lc) ->
+    (fun (a,arity,template,c,lc) ->
       let _, short_arity = decompose_prod_n_assum nparams' arity in
       let shortlc =
 	List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
       { mind_entry_typename = a;
 	mind_entry_arity = short_arity;
+	mind_entry_template = template;
 	mind_entry_consnames = c;
 	mind_entry_lc = shortlc })
     inds'
@@ -70,10 +71,10 @@ let abstract_inductive hyps nparams inds =
 
 let refresh_polymorphic_type_of_inductive (_,mip) =
   match mip.mind_arity with
-  | RegularArity s -> s.mind_user_arity
+  | RegularArity s -> s.mind_user_arity, false
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
-      mkArity (List.rev ctx, Type ar.template_level)
+      mkArity (List.rev ctx, Type ar.template_level), true
 
 let process_inductive (sechyps,abs_ctx) modlist mib =
   let nparams = mib.mind_nparams in
@@ -87,7 +88,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let inds =
     Array.map_to_list
       (fun mip ->
-	let ty = refresh_polymorphic_type_of_inductive (mib,mip) in
+	let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
 	let arity = expmod_constr modlist ty in
 	let arity = Vars.subst_instance_constr subst arity in
 	let lc = Array.map 
@@ -95,7 +96,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	  mip.mind_user_lc 
 	in
 	  (mip.mind_typename,
-	   arity,
+	   arity, template,
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 6d3dcdcb4c..4ccf794492 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -105,7 +105,7 @@ let typecheck_params_and_fields def id t ps nots fs =
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
-  let t' = match t with 
+  let t', template = match t with 
     | Some t -> 
        let env = push_rel_context newps env0 in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
@@ -113,12 +113,13 @@ let typecheck_params_and_fields def id t ps nots fs =
 	 (match kind_of_term sred with
 	 | Sort s' -> 
 	   (match Evd.is_sort_variable !evars s' with
-	   | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
-	   | None -> s)
+	   | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; 
+	     sred, true
+	   | None -> s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
       let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
-	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars)
+	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
   in
   let fullarity = it_mkProd_or_LetIn t' newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
@@ -144,7 +145,7 @@ let typecheck_params_and_fields def id t ps nots fs =
   let ce t = Evarutil.check_evars env0 Evd.empty evars t in
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
-    Evd.universe_context evars, nf arity, imps, newps, impls, newfs
+    Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =
   let id = match na with
@@ -339,8 +340,8 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite poly ctx id idbuild paramimpls params arity fieldimpls fields
-    ?(kind=StructureComponent) ?name is_coe coers sign =
+let declare_structure finite poly ctx id idbuild paramimpls params arity template 
+    fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Termops.extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
@@ -353,6 +354,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
   let mie_ind =
     { mind_entry_typename = id;
       mind_entry_arity = arity;
+      mind_entry_template = not poly && template;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] }
   in
@@ -382,8 +384,8 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-let declare_class finite def poly ctx id idbuild paramimpls params arity fieldimpls fields
-    ?(kind=StructureComponent) is_coe coers priorities sign =
+let declare_class finite def poly ctx id idbuild paramimpls params arity 
+    template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
     let len = List.length params in
@@ -422,7 +424,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
 	  cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
 	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
-	  params arity fieldimpls fields
+	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
 	in
 	let coers = List.map2 (fun coe pri -> 
@@ -510,20 +512,20 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
   (* Now, younger decl in params and fields is on top *)
-  let ctx, arity, implpars, params, implfs, fields =
+  let ctx, arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
       typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
   let sign = structure_signature (fields@params) in
     match kind with
     | Class def ->
 	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
-	  implpars params arity implfs fields is_coe coers priorities sign in
+	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
 	let ind = declare_structure finite poly ctx idstruc 
-	  idbuild implpars params arity implfs 
+	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 2422b45bd2..cead9b6f66 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -29,6 +29,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
   manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+  bool (** template arity ? *) ->
   Impargs.manual_explicitation list list -> rel_context -> (** fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
   bool -> (** coercion? *)