Ensure that side-effect declarations reaching the kernel are forced.

3 files changed, 49 insertions, 49 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d2a7703648..659f9cd1c4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -693,7 +693,7 @@ let check_signatures curmb sl =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 let constant_entry_of_side_effect eff =
   let cb = eff.seff_body in
@@ -712,7 +712,7 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEff {
-    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_body = p;
     opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
@@ -730,6 +730,25 @@ let constant_entry_of_side_effect eff =
 let export_eff eff =
   (eff.seff_constant, eff.seff_body)
 
+let is_empty_private = function
+| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx
+| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx
+
+let empty_private univs = match univs with
+| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
+
+(* Special function to call when the body of an opaque definition is provided.
+  It performs the type-checking of the body immediately. *)
+let translate_direct_opaque env kn ce =
+  let cb, ctx = Term_typing.translate_opaque env kn ce in
+  let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in
+  let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+  let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in
+  (* No constraints can be generated, we set it empty everywhere *)
+  let () = assert (is_empty_private u) in
+  { cb with const_body = OpaqueDef c }
+
 let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
@@ -760,16 +779,7 @@ let export_side_effects mb env (b_ctx, eff) =
               | DefinitionEff ce ->
                 Term_typing.translate_constant env kn (DefinitionEntry ce)
               | OpaqueEff ce ->
-                let cb, ctx = Term_typing.translate_opaque env kn ce in
-                let body = Future.force ce.Entries.opaque_entry_body in
-                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
-                let (c, u) = Term_typing.check_delayed handle ctx body in
-                let () = match u with
-                | Opaqueproof.PrivateMonomorphic ctx
-                | Opaqueproof.PrivatePolymorphic (_, ctx) ->
-                  assert (Univ.ContextSet.is_empty ctx)
-                in
-                { cb with const_body = OpaqueDef c }
+                translate_direct_opaque env kn ce
               in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
@@ -791,10 +801,7 @@ let export_private_constants ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
-    let local = match c.const_universes with
-    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
-    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
-    in
+    let local = empty_private c.const_universes in
     let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
     senv, (kn, { c with const_body = OpaqueDef o })
   | Def _ | Undef _ | Primitive _ as body ->
@@ -861,39 +868,20 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
     let cb =
       match decl with
       | OpaqueEff ce ->
-        let handle _env body () = body, Univ.ContextSet.empty, 0 in
-        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
-        let map pf = Term_typing.check_delayed handle ctx pf in
-        let pf = Future.chain ce.Entries.opaque_entry_body map in
-        { cb with const_body = OpaqueDef pf }
+        translate_direct_opaque senv.env kn ce
       | DefinitionEff ce ->
         Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
     in
-  let senv, cb, body = match cb.const_body with
-  | Def _ as const_body -> senv, { cb with const_body }, const_body
+  let senv, dcb = match cb.const_body with
+  | Def _ as const_body -> senv, { cb with const_body }
   | OpaqueDef c ->
-    let senv, o = push_opaque_proof c senv in
-    senv, { cb with const_body = OpaqueDef o }, cb.const_body
+    let local = empty_private cb.const_universes in
+    let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in
+    senv, { cb with const_body = OpaqueDef o }
   | Undef _ | Primitive _ -> assert false
   in
-  let senv = add_constant_aux senv (kn, cb) in
+  let senv = add_constant_aux senv (kn, dcb) in
   let eff =
-    let body, univs = match body with
-    | (Primitive _ | Undef _) -> assert false
-    | Def c -> (Def c, cb.const_universes)
-    | OpaqueDef o ->
-      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, 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
     let eff = {
       from_env = from_env;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c60e7e893f..ec86495db8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ type global_declaration =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 type exported_private_constant = Constant.t
 
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c9da88988f..63a93d3dc3 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -204,11 +204,11 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
-| PureEntry : unit effect_entry
+type ('a, 'b) effect_entry =
+| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
+| PureEntry : (unit, Constr.constr) effect_entry
 
-let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry) =
+let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -238,12 +238,24 @@ let cast_opaque_proof_entry (type a) (entry : a effect_entry) (e : a proof_entry
     Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
   | Some hyps -> hyps
   in
+  let (body, univs : b * _) = match entry with
+  | PureEntry ->
+    let (body, uctx), () = Future.force e.proof_entry_body in
+    let univs = match e.proof_entry_universes with
+    | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx')
+    | Polymorphic_entry _ ->
+      assert (Univ.ContextSet.is_empty uctx);
+      e.proof_entry_universes
+    in
+    body, univs
+  | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
+  in
   {
-    opaque_entry_body = e.proof_entry_body;
+    opaque_entry_body = body;
     opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
-    opaque_entry_universes = e.proof_entry_universes;
+    opaque_entry_universes = univs;
   }
 
 let get_roles export eff =