Adding a local type-in-type flag in kernel declarations.

6 files changed, 16 insertions, 0 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 8b42a90e48..639cd061bc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -73,6 +73,7 @@ type constant_universes = Univ.universe_context
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_universes : bool; (** If [false] universe constraints are not checked *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
@@ -192,6 +193,9 @@ type mutual_inductive_body = {
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
   
     mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
+
+    mind_unsafe_universes : bool; (** generated with the type-in-type flag *)
+
 }
 
 (** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 28f7e69cd4..5caf052ace 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -16,6 +16,7 @@ open Context.Rel.Declaration
 
 let safe_flags = {
   check_guarded = true;
+  check_universes = true;
 }
 
 (** {6 Arities } *)
@@ -261,6 +262,7 @@ let subst_mind_body sub mib =
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_checked_positive = mib.mind_checked_positive;
+    mind_unsafe_universes = mib.mind_unsafe_universes;
   }
 
 let inductive_instance mib =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d8493d9baf..032e713593 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,6 +328,9 @@ let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_constant cst env
 
+let type_in_type_constant cst env =
+  not (lookup_constant cst env).const_typing_flags.check_universes
+
 let template_polymorphic_constant cst env =
   match (lookup_constant cst env).const_type with 
   | TemplateArity _ -> true
@@ -357,6 +360,9 @@ let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_ind ind env
 
+let type_in_type_ind (mind,i) env =
+  (lookup_mind mind env).mind_unsafe_universes
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | TemplateArity _ -> true
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5203899546..7ce1cea272 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -136,6 +136,7 @@ val evaluable_constant : constant -> env -> bool
 (** New-style polymorphism *)
 val polymorphic_constant  : constant -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
+val type_in_type_constant : constant -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_constant  : constant -> env -> bool
@@ -183,6 +184,7 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
 val polymorphic_pind : pinductive -> env -> bool
+val type_in_type_ind : inductive -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_ind : inductive -> env -> bool
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b74788d217..34771034cc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -923,6 +923,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
       mind_universes = ctx;
       mind_private = prv;
       mind_checked_positive = is_checked;
+      mind_unsafe_universes = type_in_type env;
     }
 
 (************************************************************************)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f0c116d275..a7c6ef0572 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -269,6 +269,7 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+  let flags = { flags with check_universes = flags.check_universes && not (type_in_type env) } in
   let open Context.Named.Declaration in
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in