Specific code path for opaque polymorphic constants.

For now this is just a specialized version of the previous generic code.
This simplifies tracking of the changes.

1 files changed, 47 insertions, 21 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index eea04bbf9a..5395fec2c6 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,19 +157,59 @@ the polymorphic case
         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
+  (** 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 () = assert (not (opaque && Option.is_empty typ)) in
       let (body, ctx), side_eff = Future.join body in
       let body, ctx = match trust with
       | Pure -> body, ctx
       | SideEffects handle ->
-        let () = assert opaque in
         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_context ~strict:false uctx env in
+      let sbst, auctx = Univ.abstract_universes nas uctx in
+      let usubst = Univ.make_instance_subst sbst in
+      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 typ =
+        let tj = Typeops.infer_type env typ in
+        let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+        Vars.subst_univs_level_constr usubst tj.utj_val
+      in
+      let def = Vars.subst_univs_level_constr usubst j.uj_val in
+      let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) 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 = Retypeops.relevance_of_term env j.uj_val;
+        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; _ } = c in
+      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c 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 ->
+        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 ->
         let ctx = Univ.ContextSet.union univs ctx in
@@ -190,9 +222,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
@@ -208,10 +237,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;