Let definitions do not create new universe constraints.

We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.

8 files changed, 45 insertions, 50 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index ae28c4b90..5be07e09e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -231,19 +231,24 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let (de, eff) = Global.export_private_constants ~in_section:true de in
       let () = List.iter register_side_effect eff in
-      let body = Future.chain de.const_entry_body (fun (body, ()) -> body) in
+      (** The body should already have been forced upstream because it is a
+          section-local definition, but it's not enforced by typing *)
+      let (body, uctx), () = Future.force de.const_entry_body in
+      let poly, univs = match de.const_entry_universes with
+      | Monomorphic_const_entry uctx -> false, uctx
+      | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
+      in
+      let univs = Univ.ContextSet.union uctx univs in
+      (** We must declare the universe constraints before type-checking the
+          term. *)
+      let () = Global.push_context_set (not poly) univs in
       let se = {
         secdef_body = body;
         secdef_secctx = de.const_entry_secctx;
-        secdef_universes = de.const_entry_universes;
         secdef_feedback = de.const_entry_feedback;
         secdef_type = de.const_entry_type;
       } in
-      let univs = Global.push_named_def (id, se) in
-      let poly = match de.const_entry_universes with
-      | Monomorphic_const_entry _ -> false
-      | Polymorphic_const_entry _ -> true
-      in
+      let () = Global.push_named_def (id, se) in
       Explicit, de.const_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 35a158682..36b75668b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -82,11 +82,10 @@ type 'a definition_entry = {
   const_entry_inline_code : bool }
 
 type section_def_entry = {
-  secdef_body : constr Univ.in_universe_context_set Future.computation;
+  secdef_body : constr;
   secdef_secctx : Context.Named.t option;
   secdef_feedback : Stateid.t option;
   secdef_type : types option;
-  secdef_universes : constant_universes_entry;
 }
 
 type inline = int option (* inlining level, None for no inlining *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4fbe02cf5..93b8e278f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,22 +382,9 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let open Entries in
-  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let poly = match de.Entries.secdef_universes with
-  | Monomorphic_const_entry _ -> false
-  | Polymorphic_const_entry _ -> true
-  in
-  let c, univs = match c with
-    | Def c -> Mod_subst.force_constr c, univs
-    | OpaqueDef o ->
-        Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
-        Univ.ContextSet.union univs 
-	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
-    | _ -> assert false in
-  let senv' = push_context_set poly univs senv in
-  let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
-    univs, {senv' with env=env''}
+  let c, typ = Term_typing.translate_local_def senv.env id de in
+  let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in
+  { senv with env = env'' }
 
 let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index faa758d07..757b803a3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.section_def_entry -> Univ.ContextSet.t safe_transformer
+  Id.t * Entries.section_def_entry -> safe_transformer0
 
 (** Insertion of global axioms or definitions *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c2c65d6d4..2e4426d62 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -227,17 +227,14 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       feedback ~id:state_id Feedback.Complete)
 
-let abstract_constant_universes abstract = function
+let abstract_constant_universes = function
   | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
   | Polymorphic_const_entry uctx ->
-    if not abstract then
-      Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
-    else
-      let sbst, auctx = Univ.abstract_universes uctx in
-      sbst, Polymorphic_const auctx
+    let sbst, auctx = Univ.abstract_universes uctx in
+    sbst, Polymorphic_const auctx
 
-let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
+let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -245,10 +242,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
         | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
       in
       let j = infer env t in
-      let abstract = not (Option.is_empty kn) in
-      let usubst, univs = 
-        abstract_constant_universes abstract uctx
-      in
+      let usubst, univs = abstract_constant_universes uctx in
       let c = Typeops.assumption_of_judgment env j in
       let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
       {
@@ -316,12 +310,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       | SideEffects _ -> inline_side_effects env body ctx side_eff
       in
       let env = push_context_set ~strict:(not poly) ctx env in
-      let abstract = not (Option.is_empty kn) in
       let ctx = if poly
         then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
         else Monomorphic_const_entry ctx
       in
-      let usubst, univs = abstract_constant_universes abstract ctx in
+      let usubst, univs = abstract_constant_universes ctx in
       let j = infer env body in
       let typ = match typ with
         | None ->
@@ -493,7 +486,7 @@ let build_constant_declaration kn env result =
 
 let translate_constant mb env kn ce =
   build_constant_declaration kn env
-    (infer_declaration ~trust:mb env (Some kn) ce)
+    (infer_declaration ~trust:mb env ce)
 
 let constant_entry_of_side_effect cb u =
   let univs =
@@ -607,17 +600,17 @@ let translate_recipe env kn r =
 
 let translate_local_def env id centry =
   let open Cooking in
-  let body = Future.chain centry.secdef_body (fun body -> body, ()) in
+  let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in
   let centry = {
     const_entry_body = body;
     const_entry_secctx = centry.secdef_secctx;
     const_entry_feedback = centry.secdef_feedback;
     const_entry_type = centry.secdef_type;
-    const_entry_universes = centry.secdef_universes;
+    const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
     const_entry_opaque = false;
     const_entry_inline_code = false;
   } in
-  let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
+  let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
   let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with
@@ -629,11 +622,22 @@ let translate_local_def env id centry =
          (Opaqueproof.force_proof (opaque_tables env) lc) in
        record_aux env ids_typ ids_def
   end;
-  let univs = match decl.cook_universes with
-  | Monomorphic_const ctx -> ctx
+  let () = match decl.cook_universes with
+  | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
   | Polymorphic_const _ -> assert false
   in
-  decl.cook_body, typ, univs
+  let c = match decl.cook_body with
+  | Def c -> Mod_subst.force_constr c
+  | OpaqueDef o ->
+    let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
+    let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+    (** Let definitions are ensured to have no extra constraints coming from
+        the body by virtue of the typing of [Entries.section_def_entry]. *)
+    let () = assert (Univ.ContextSet.is_empty cst) in
+    p
+  | Undef _ -> assert false
+  in
+  c, typ
 
 (* Insertion of inductive types. *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 4b893b056..7bc029010 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
-  constant_def * types * Univ.ContextSet.t
+  constr * types
 
 val translate_local_assum : env -> types -> types
 
@@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env -> Constant.t option -> 
+val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
diff --git a/library/global.ml b/library/global.ml
index ce37dfecf..ed847b7cd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -81,7 +81,7 @@ let globalize_with_summary fs f =
 let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize (Safe_typing.push_named_def d)
+let push_named_def d = globalize0 (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
diff --git a/library/global.mli b/library/global.mli
index 5d7495657..03bc945da 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.section_def_entry) -> Univ.ContextSet.t
+val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.definition_entry ->