Cleaning up the previous code by ensuring statically invariants on opaque proofs.

We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.

6 files changed, 75 insertions, 87 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 1e6bc14935..8c4bd16ae3 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -102,11 +102,10 @@ type 'a const_entry_body = 'a proof_output Future.computation
 (** 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
+type constant_entry =
+  | DefinitionEntry : definition_entry -> constant_entry
+  | ParameterEntry : parameter_entry -> constant_entry
+  | PrimitiveEntry : primitive_entry -> constant_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4dbc009324..43aafac809 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -299,13 +299,6 @@ let lift_constant c =
   in
   { c with const_body = body }
 
-let map_constant f c =
-  let body = match c.const_body with
-  | OpaqueDef o -> OpaqueDef (f o)
-  | Def _ | Undef _ | Primitive _ as body -> body
-  in
-  { c with const_body = body }
-
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
@@ -585,7 +578,8 @@ type 'a effect_entry =
 | PureEntry : unit effect_entry
 
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
@@ -765,17 +759,14 @@ let export_side_effects mb env (b_ctx, eff) =
           if Int.equal sl 0 then
             let env, cb =
               let kn = eff.seff_constant in
-               let ce = constant_entry_of_side_effect eff in
-               let open Entries in
-               let cb = match ce with
-               | DefinitionEff ce ->
+              let ce = constant_entry_of_side_effect eff in
+              let open Entries in
+              let cb = match ce with
+              | DefinitionEff ce ->
                 Term_typing.translate_constant env kn (DefinitionEntry ce)
-               | OpaqueEff ce ->
-                Term_typing.translate_constant env kn (OpaqueEntry ce)
-               in
-              let map ctx = match ce with
-              | OpaqueEff e ->
-                let body = Future.force e.Entries.opaque_entry_body in
+              | 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
@@ -783,10 +774,8 @@ let export_side_effects mb env (b_ctx, eff) =
                 | Opaqueproof.PrivatePolymorphic (_, ctx) ->
                   assert (Univ.ContextSet.is_empty ctx)
                 in
-                c
-              | _ -> assert false
+                { cb with const_body = OpaqueDef c }
               in
-               let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
@@ -826,23 +815,18 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
-      | ConstantEntry (EffectEntry, Entries.OpaqueEntry e) ->
+      | OpaqueEntry ce ->
         let handle env body eff =
           let body, uctx, signatures = inline_side_effects env body eff in
           let trusted = check_signatures senv.revstruct signatures in
           body, uctx, trusted
         in
-        let cb = Term_typing.translate_constant senv.env kn (Entries.OpaqueEntry e) in
-        let ctx = match cb.const_body with
-        | OpaqueDef ctx -> ctx
-        | _ -> assert false
-        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 e.Entries.opaque_entry_body map in
+        let pf = Future.chain ce.Entries.opaque_entry_body map in
         { cb with const_body = OpaqueDef pf }
-      | ConstantEntry (PureEntry, ce) ->
-        let cb = Term_typing.translate_constant senv.env kn ce in
-        map_constant (fun _ -> assert false) cb
+      | ConstantEntry ce ->
+        Term_typing.translate_constant senv.env kn ce
     in
   let senv =
     let senv, cb, delayed_cst = match cb.const_body with
@@ -870,7 +854,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
 
   let senv =
     match decl with
-    | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
+    | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) ->
       if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b55293f1c..6e5c9c55ae 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -78,7 +78,8 @@ type 'a effect_entry =
 | PureEntry : unit effect_entry
 
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1e0db8026f..f85b3db413 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -64,7 +64,7 @@ type typing_context =
 | MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option
 | PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
 
-let infer_declaration (type a) env (dcl : a constant_entry) =
+let infer_declaration env (dcl : constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -112,47 +112,6 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_relevance = Sorts.Relevant;
       }
 
-  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
-      let env = push_context_set ~strict:true univs env in
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let tyj = Typeops.infer_type env typ in
-      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      {
-        Cooking.cook_body = def;
-        cook_type = tyj.utj_val;
-        cook_universes = Monomorphic univs;
-        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Similar case for polymorphic entries. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
-      let { opaque_entry_feedback = feedback_id; _ } = c in
-      let env = push_context ~strict:false uctx env in
-      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 context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
-      let def = OpaqueDef context in
-      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-      {
-        Cooking.cook_body = def;
-        cook_type = typ;
-        cook_universes = Polymorphic auctx;
-        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
@@ -189,6 +148,43 @@ let infer_declaration (type a) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
+(** Definition is opaque (Qed), so we delay the typing of its body. *)
+let infer_opaque env = function
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
+      let env = push_context_set ~strict:true univs env in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let tyj = Typeops.infer_type env typ in
+      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      {
+        Cooking.cook_body = def;
+        cook_type = tyj.utj_val;
+        cook_universes = Monomorphic univs;
+        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let env = push_context ~strict:false uctx env in
+      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 context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_universes = Polymorphic auctx;
+        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
 let check_section_variables env declared_set typ body =
   let ids_typ = global_vars_set env typ in
   let ids_def = global_vars_set env body in
@@ -297,6 +293,10 @@ let translate_constant env _kn ce =
   build_constant_declaration env
     (infer_declaration env ce)
 
+let translate_opaque env _kn ce =
+  let def, ctx = infer_opaque env ce in
+  build_constant_declaration env def, ctx
+
 let translate_local_assum env t =
   let j = Typeops.infer env t in
   let t = Typeops.assumption_of_judgment env j in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index f82312245b..c9f6d66e36 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,8 +30,12 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  env -> Constant.t -> 'a constant_entry ->
-    typing_context constant_body
+  env -> Constant.t -> constant_entry ->
+    'a constant_body
+
+val translate_opaque :
+  env -> Constant.t -> 'a opaque_entry ->
+    unit constant_body * typing_context
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
@@ -40,7 +44,7 @@ val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (C
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : env ->
-  'a constant_entry -> typing_context Cooking.result
+  constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 61321cd605..719430e71c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -259,17 +259,17 @@ let define_constant ~side_effect ~name cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = Entries.DefinitionEntry (cast_proof_entry de) in
-      export, ConstantEntry (PureEntry, cd), false
+      export, ConstantEntry cd, false
     else
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
       let de = cast_opaque_proof_entry de in
-      [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false
+      [], OpaqueEntry de, false
   | ParameterEntry e ->
-    [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+    [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
   | PrimitiveEntry e ->
-    [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
+    [], ConstantEntry (Entries.PrimitiveEntry e), false
   in
   let kn, eff = Global.add_constant ~side_effect name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();