Merge PR #10252: Various dynamic assertions and cleanups in opaque typing

Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot

3 files changed, 57 insertions, 26 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1bc5891517..dedbddfee0 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,13 +29,13 @@ let check_constant_declaration env kn cb =
       let env = push_context ~strict:false ctx env in
       true, env
   in
+  let ty = cb.const_type in
+  let _ = infer_type env' ty in
   let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
     | None, _ -> env'
     | Some local, (OpaqueDef _, true) -> push_subgraph local env'
     | Some _, _ -> assert false
   in
-  let ty = cb.const_type in
-  let _ = infer_type env' ty in
   let otab = Environ.opaque_tables env in
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 088dd98db8..f984088f47 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -115,16 +115,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       }
 
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body.
-      Remark: when the universe quantification is given explicitly, we could
-      delay even in the polymorphic case.  *)
+      so we delay the typing and hash consing of its body. *)
 
-(** Definition is opaque (Qed) and non polymorphic with known type, so we delay
-the typing and hash consing of its body.
-
-TODO: if the universe quantification is given explicitly, we could delay even in
-the polymorphic case
-  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
                        const_entry_universes = Monomorphic_entry univs; _ } as c) ->
@@ -165,16 +157,59 @@ the polymorphic case
         cook_context = c.const_entry_secctx;
       }
 
+  (** Similar case for polymorphic entries. TODO: also delay type-checking of
+      the body. *)
+
+  | DefinitionEntry ({ const_entry_type = Some typ;
+                       const_entry_opaque = true;
+                       const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { const_entry_body = body; const_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 (def, private_univs) =
+        let (body, ctx), side_eff = Future.join body in
+        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
+        (** [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
+        let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
+        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 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;
+      }
+
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
-      let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in
+      let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      let (body, ctx), side_eff = Future.join body in
+      (* Opaque constants must be provided with a non-empty const_entry_type,
+         and thus should have been treated above. *)
+      let () = assert (not c.const_entry_opaque) in
       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'
+      | Pure ->
+        let (body, ctx), () = Future.join body in
+        body, ctx
+      | SideEffects _ -> assert false
       in
       let env, usubst, univs, private_univs = match c.const_entry_universes with
       | Monomorphic_entry univs ->
@@ -188,9 +223,6 @@ the polymorphic case
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
         let env, local =
-          if opaque then
-            push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
-          else
           if Univ.ContextSet.is_empty ctx then env, None
           else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
@@ -206,10 +238,7 @@ the polymorphic case
            Vars.subst_univs_level_constr usubst tj.utj_val
       in
       let def = Vars.subst_univs_level_constr usubst j.uj_val in
-      let def = 
-        if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
-	else Def (Mod_subst.from_val def) 
-      in
+      let def = Def (Mod_subst.from_val def) in
 	feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index aeceeb4e50..8e7b045b8e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,9 +153,11 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let univs = Monomorphic_entry univs in
+  let () = Declare.declare_universe_context false univs in
+  let types = (Typeops.infer (Global.env ()) c).uj_type in
+  let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
-            (DefinitionEntry (definition_entry ~opaque:true ~univs c),
+            (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
 	     IsProof Lemma))
 
 (* Calling a global tactic *)