Merge PR #10439: Uniform handling of side-effects for opaque definitions

Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes

5 files changed, 39 insertions, 39 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index bc389e9fcf..47e2f72b0e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,11 +99,14 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-type 'a constant_entry =
-  | DefinitionEntry of definition_entry
-  | OpaqueEntry of 'a const_entry_body opaque_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
+(** Dummy wrapper type discriminable from unit *)
+type 'a seff_wrap = { seff_wrap : 'a }
+
+type _ constant_entry =
+  | DefinitionEntry : definition_entry -> unit constant_entry
+  | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry
+  | ParameterEntry : parameter_entry -> unit constant_entry
+  | PrimitiveEntry : primitive_entry -> unit constant_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 24b3765019..ea45f699ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -527,7 +527,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
+| EffectEntry : private_constants Entries.seff_wrap effect_entry
 | PureEntry : unit effect_entry
 
 type global_declaration =
@@ -669,6 +669,9 @@ let check_signatures curmb sl =
   | None -> 0
   | Some (n, _) -> n
 
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
 
 let constant_entry_of_side_effect eff =
   let cb = eff.seff_body in
@@ -686,7 +689,7 @@ let constant_entry_of_side_effect eff =
     | Def b -> Mod_subst.force_constr b
     | _ -> assert false in
   if Declareops.is_opaque cb then
-  OpaqueEntry {
+  OpaqueEff {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
     opaque_entry_secctx = cb.const_hyps;
     opaque_entry_feedback = None;
@@ -694,7 +697,7 @@ let constant_entry_of_side_effect eff =
     opaque_entry_universes = univs;
   }
   else
-  DefinitionEntry {
+  DefinitionEff {
     const_entry_body = p;
     const_entry_secctx = Some cb.const_hyps;
     const_entry_feedback = None;
@@ -730,7 +733,15 @@ let export_side_effects mb env (b_ctx, eff) =
             let env, cb =
               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 open Entries in
+               let open Term_typing in
+               let cb = match ce with
+               | DefinitionEff ce ->
+                Term_typing.translate_constant Pure env kn (DefinitionEntry ce)
+               | OpaqueEff ce ->
+                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+                Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce)
+               in
               let map cu =
                 let (c, u) = Future.force cu in
                 let () = match u with
@@ -822,7 +833,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
       seff_constant = kn;
       seff_body = cb;
     } in
-    SideEffects.add eff empty_private_constants
+    { Entries.seff_wrap = SideEffects.add eff empty_private_constants }
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c3d0965857..2406b6add1 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -79,7 +79,7 @@ val push_named_def :
 (** Insertion of global axioms or definitions *)
 
 type 'a effect_entry =
-| EffectEntry : private_constants effect_entry
+| EffectEntry : private_constants Entries.seff_wrap effect_entry
 | PureEntry : unit effect_entry
 
 type global_declaration =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 5844bd89f8..b65e62ba30 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -31,7 +31,7 @@ type 'a effect_handler =
 
 type _ trust =
 | Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a trust
+| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
 
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
@@ -124,22 +124,14 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         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
-          | Pure ->
-            let env = push_context_set uctx env in
-            let j = Typeops.infer env body in
-            let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
-            j, uctx
-          | SideEffects handle ->
-            let (body, uctx', valid_signatures) = handle env body side_eff in
-            let uctx = Univ.ContextSet.union uctx uctx' in
-            let env = push_context_set uctx env in
-            let body,env,ectx = skip_trusted_seff valid_signatures body env in
-            let j = Typeops.infer env body in
-            let j = unzip ectx j in
-            let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
-            j, uctx
-          in
+          let SideEffects handle = trust in
+          let (body, uctx', valid_signatures) = handle env body side_eff in
+          let uctx = Univ.ContextSet.union uctx uctx' in
+          let env = push_context_set uctx env in
+          let body,env,ectx = skip_trusted_seff valid_signatures body env in
+          let j = Typeops.infer env body in
+          let j = unzip ectx j in
+          let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
           let c = j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, Opaqueproof.PrivateMonomorphic uctx
@@ -164,12 +156,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let sbst, auctx = Univ.abstract_universes nas uctx in
       let usubst = Univ.make_instance_subst sbst in
       let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
-        let body, ctx = match trust with
-        | Pure -> body, ctx
-        | SideEffects handle ->
-          let body, ctx', _ = handle env body side_eff in
-          body, Univ.ContextSet.union ctx ctx'
-        in
+        let SideEffects handle = trust in
+        let body, ctx', _ = handle env body side_eff in
+        let ctx = Univ.ContextSet.union ctx ctx' in
         (** [ctx] must contain local universes, such that it has no impact
             on the rest of the graph (up to transitivity). *)
         let env = push_subgraph ctx env in
@@ -195,10 +184,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      let () = match trust with
-      | Pure -> ()
-      | SideEffects _ -> assert false
-      in
+      let Pure = trust in
       let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry ctx ->
         let env = push_context_set ~strict:true ctx env in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 225abd60f8..ef01ece185 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -24,7 +24,7 @@ type 'a effect_handler =
 
 type _ trust =
 | Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a trust
+| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * Sorts.relevance * types