Merge PR #6469: No universe constraints in Let definitions

5 files changed, 46 insertions, 38 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404..36b75668b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,13 @@ type 'a definition_entry = {
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
+type section_def_entry = {
+  secdef_body : constr;
+  secdef_secctx : Context.Named.t option;
+  secdef_feedback : Stateid.t option;
+  secdef_type : types option;
+}
+
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fa984515a..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.const_entry_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 fbc398a2a..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 * unit Entries.definition_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 761eab511..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,7 +600,17 @@ let translate_recipe env kn r =
 
 let translate_local_def env id centry =
   let open Cooking in
-  let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) 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 = Monomorphic_const_entry Univ.ContextSet.empty;
+    const_entry_opaque = false;
+    const_entry_inline_code = false;
+  } 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
@@ -619,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 c771452a1..7bc029010 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,8 +18,8 @@ type _ trust =
 | Pure : unit trust
 | SideEffects : structure_body -> side_effects trust
 
-val translate_local_def : env -> Id.t -> unit definition_entry ->
-  constant_def * types * Univ.ContextSet.t
+val translate_local_def : env -> Id.t -> section_def_entry ->
+  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 :