Allow to delay polymorphic opaque constants.

We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.

9 files changed, 113 insertions, 76 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1336e3e8bf..fbc0822570 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -159,7 +159,6 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
@@ -202,7 +201,7 @@ let lift_univs cb subst auctx0 =
     let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
     subst, (Polymorphic auctx)
 
-let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, (c, priv)) =
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let ainst = Instance.of_array (Array.init univs Level.var) in
@@ -211,7 +210,15 @@ let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
   let c = abstract_constant_body (expmod c) hyps in
-  univs + AUContext.size abs_ctx, c
+  let priv = match priv with
+  | Opaqueproof.PrivateMonomorphic () ->
+    let () = assert (AUContext.is_empty abs_ctx) in
+    priv
+  | Opaqueproof.PrivatePolymorphic ctx ->
+    let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in
+    Opaqueproof.PrivatePolymorphic ctx
+  in
+  univs + AUContext.size abs_ctx, (c, priv)
 
 let cook_constr infos univs c =
   let fold info (univs, c) = cook_constr info (univs, c) in
@@ -240,15 +247,10 @@ let cook_constant { from = cb; info } =
 		  hyps)
       hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
-  let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
-                                            (Univ.make_instance_subst usubst)))
-      cb.const_private_poly_univs
-  in
   {
     cook_body = body;
     cook_type = typ;
     cook_universes = univs;
-    cook_private_univs = private_univs;
     cook_relevance = cb.const_relevance;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 934b7c6b50..c98fb0bc3a 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,14 +21,14 @@ type 'opaque result = {
   cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
-  cook_private_univs : Univ.ContextSet.t option;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
   cook_context : Constr.named_context option;
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int ->
+  (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
 
 val cook_inductive :
   Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 388b4f14bf..deb01589b6 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,7 +94,6 @@ type 'opaque constant_body = {
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : universes;
-    const_private_poly_univs : Univ.ContextSet.t option;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index de9a052096..a8ebed2326 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -113,7 +113,6 @@ let subst_const_body sub cb =
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
-        const_private_poly_univs = cb.const_private_poly_univs;
         const_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;
         const_typing_flags = cb.const_typing_flags }
@@ -144,16 +143,11 @@ let hcons_universes cbu =
   | Polymorphic ctx ->
     Polymorphic (Univ.hcons_abstract_universe_context ctx)
 
-let hcons_const_private_univs = function
-  | None -> None
-  | Some univs -> Some (Univ.hcons_universe_context_set univs)
-
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = Constr.hcons cb.const_type;
     const_universes = hcons_universes cb.const_universes;
-    const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
   }
 
 (** {6 Inductive types } *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 472fddb829..fcd88fd543 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver =
     let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-        const_private_poly_univs = None;
 	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index e18b726111..66c50c4b57 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -20,13 +20,24 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
 type indirect_accessor = {
-  access_proof : DirPath.t -> int -> constr option;
-  access_discharge : cooking_info list -> int -> constr -> constr;
+  access_proof : DirPath.t -> int -> opaque_proofterm;
+  access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+let drop_mono = function
+| PrivateMonomorphic _ -> PrivateMonomorphic ()
+| PrivatePolymorphic _ as ctx -> ctx
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type universes = int
+
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of universes * cooking_info list * proofterm
@@ -59,7 +70,10 @@ let turn_indirect dp o tab = match o with
       hashconsing of their contents, potentially as a future. *)
       let hcons (c, u) =
         let c = Constr.hcons c in
-        let u = Univ.hcons_universe_context_set u in
+        let u = match u with
+        | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+        | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u)
+        in
         (c, u)
       in
       let cu = Future.chain cu hcons in
@@ -97,34 +111,42 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
 
 let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (n, d, cu) ->
-    let (c, _) = Future.force cu in
-    access.access_discharge d n c
+    let (c, u) = Future.force cu in
+    access.access_discharge d n (c, drop_mono u)
   | Indirect (l,dp,i) ->
-      let c =
+      let c, u =
         if DirPath.equal dp odp
         then
           let (n, d, cu) = Int.Map.find i prfs in
-          let (c, _) = Future.force cu in
-          access.access_discharge d n c
-        else match access.access_proof dp i with
-        | None -> not_here ()
-        | Some v -> v
+          let (c, u) = Future.force cu in
+          access.access_discharge d n (c, drop_mono u)
+        else
+          let (n, d, cu) = access.access_proof dp i in
+          match cu with
+          | None -> not_here ()
+          | Some (c, u) -> access.access_discharge n d (c, u)
       in
-      force_constr (List.fold_right subst_substituted l (from_val c))
+      let c = force_constr (List.fold_right subst_substituted l (from_val c)) in
+      (c, u)
+
+let get_mono (_, u) = match u with
+| PrivateMonomorphic ctx -> ctx
+| PrivatePolymorphic _ -> Univ.ContextSet.empty
 
 let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,_,cu) ->
-    snd(Future.force cu)
+    get_mono (Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then
         let (_, _, cu) = Int.Map.find i prfs in
-        snd (Future.force cu)
+        get_mono (Future.force cu)
       else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, _, cu) -> Future.chain cu snd
+| Direct (_, _, cu) ->
+  Future.chain cu get_mono
 
 module FMap = Future.UUIDMap
 
@@ -136,8 +158,14 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     let c =
       if Future.is_val cu then
-        let (c, _) = Future.force cu in
-        Some c
+        let (c, priv) = Future.force cu in
+        let priv = match priv with
+        | PrivateMonomorphic _ ->
+          let () = assert (Int.equal univs 0) in
+          PrivateMonomorphic ()
+        | PrivatePolymorphic _ as priv -> priv
+        in
+        Some (c, priv)
       else if Future.UUIDSet.mem uid except then None
       else
         CErrors.anomaly
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 6e275649cd..20c862c651 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -21,7 +21,11 @@ open Mod_subst
     When it is [turn_indirect] the data is relocated to an opaque table
     and the [opaque] is turned into an index. *)
 
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
 type opaquetab
 type opaque
 
@@ -42,9 +46,12 @@ type cooking_info = {
   modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
 type indirect_accessor = {
-  access_proof : DirPath.t -> int -> constr option;
-  access_discharge : cooking_info list -> int -> constr -> constr;
+  access_proof : DirPath.t -> int -> opaque_proofterm;
+  access_discharge : cooking_info list -> int ->
+    (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -53,7 +60,7 @@ type indirect_accessor = {
 
 (** From a [opaque] back to a [constr]. This might use the
     indirect opaque accessor given as an argument. *)
-val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes
 val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
@@ -65,5 +72,5 @@ val discharge_direct_opaque :
 val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
-  (cooking_info list * int * Constr.t option) array *
+  opaque_proofterm array *
   int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0b0f14eee7..596fcd210c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -725,11 +725,14 @@ let export_side_effects mb env (b_ctx, eff) =
               let kn = eff.seff_constant in
                let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let map cu =
+              let map cu =
                 let (c, u) = Future.force cu in
-                let () = assert (Univ.ContextSet.is_empty u) in
+                let () = match u with
+                | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+                  assert (Univ.ContextSet.is_empty ctx)
+                in
                 c
-               in
+              in
                let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
@@ -742,13 +745,16 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
-let n_univs cb = match cb.const_universes with
-| Monomorphic _ -> 0
-| Polymorphic auctx -> Univ.AUContext.size auctx
-
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
+  let map univs p =
+    let univs, local = match univs with
+    | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+    | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    in
+    Opaqueproof.create ~univs (Future.from_val (p, local))
+  in
+  let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
   let bodies = List.map map exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -775,7 +781,11 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
+    let univs = match cb.const_universes with
+    | Monomorphic _ -> 0
+    | Polymorphic auctx -> Univ.AUContext.size auctx
+    in
+    let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -791,14 +801,16 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
     | OpaqueDef o ->
-      let (b, ctx) = Future.force o in
-      match cb.const_universes with
-      | Monomorphic ctx' ->
+      let (b, delayed) = Future.force o in
+      match cb.const_universes, delayed with
+      | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
         OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx ->
+      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx ->
         (* Upper layers enforce that there are no internal constraints *)
         let () = assert (Univ.ContextSet.is_empty ctx) in
         OpaqueDef b, Polymorphic auctx
+      | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
+        assert false
     in
     let cb = { cb with const_body = body; const_universes = univs } in
     let from_env = CEphemeron.create senv.revstruct in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f984088f47..9ec3269375 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -79,7 +79,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = Undef nl;
         cook_type = t;
         cook_universes = univs;
-        cook_private_univs = None;
         cook_relevance = r;
         cook_inline = false;
         cook_context = ctx;
@@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       { Cooking.cook_body = cd;
         cook_type = ty;
         cook_universes = Monomorphic uctxt;
-        cook_private_univs = None;
         cook_inline = false;
         cook_context = None;
         cook_relevance = Sorts.Relevant;
@@ -124,7 +122,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       let tyj = Typeops.infer_type env typ in
       let proofterm =
-        Future.chain body (fun ((body,uctx),side_eff) ->
+        Future.chain body begin fun ((body,uctx),side_eff) ->
           (* don't redeclare universes which are declared for the type *)
           let uctx = Univ.ContextSet.diff uctx univs in
           let j, uctx = match trust with
@@ -145,13 +143,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
           in
           let c = j.uj_val in
           feedback_completion_typecheck feedback_id;
-          c, uctx) in
+          c, Opaqueproof.PrivateMonomorphic uctx
+      end in
       let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
         cook_universes = Monomorphic univs;
-        cook_private_univs = None;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -168,8 +166,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let tj = Typeops.infer_type env typ in
       let sbst, auctx = Univ.abstract_universes nas uctx in
       let usubst = Univ.make_instance_subst sbst in
-      let (def, private_univs) =
-        let (body, ctx), side_eff = Future.join body in
+      let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
         let body, ctx = match trust with
         | Pure -> body, ctx
         | SideEffects handle ->
@@ -183,16 +180,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let j = Typeops.infer env body in
         let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
         let def = Vars.subst_univs_level_constr usubst j.uj_val in
-        def, private_univs
-      in
-      let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+        let () = feedback_completion_typecheck feedback_id in
+        def, Opaqueproof.PrivatePolymorphic private_univs
+      end in
+      let def = OpaqueDef proofterm in
       let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-        feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = Polymorphic auctx;
-        cook_private_univs = Some private_univs;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -211,22 +207,22 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         body, ctx
       | SideEffects _ -> assert false
       in
-      let env, usubst, univs, private_univs = match c.const_entry_universes with
+      let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry univs ->
         let ctx = Univ.ContextSet.union univs ctx in
         let env = push_context_set ~strict:true ctx env in
-        env, Univ.empty_level_subst, Monomorphic ctx, None
+        env, Univ.empty_level_subst, Monomorphic ctx
       | Polymorphic_entry (nas, uctx) ->
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        let env, local =
-          if Univ.ContextSet.is_empty ctx then env, None
-          else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+        let () =
+          if not (Univ.ContextSet.is_empty ctx) then
+            CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
-        env, sbst, Polymorphic auctx, local
+        env, sbst, Polymorphic auctx
       in
       let j = Typeops.infer env body in
       let typ = match typ with
@@ -244,7 +240,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
-        cook_private_univs = private_univs;
         cook_relevance = Retypeops.relevance_of_term env j.uj_val;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -341,7 +336,6 @@ let build_constant_declaration env result =
     const_type = typ;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -368,7 +362,6 @@ let translate_recipe env _kn r =
     const_type = result.cook_type;
     const_body_code = tps;
     const_universes = univs;
-    const_private_poly_univs = result.cook_private_univs;
     const_relevance = result.cook_relevance;
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
@@ -407,7 +400,10 @@ let translate_local_def env _id centry =
     let (p, cst) = Future.force 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
+    let () = match cst with
+    | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+    in
     p
   | Undef _ | Primitive _ -> assert false
   in