Enforce that polymorphic definitions do not generate internal constraints.

In practice, we only send to the kernel polymorphic definitions whose
side-effects have been exported first, and furthermore their bodies have
already been forced. Therefore, no constraints are generated by the kernel.

Nonetheless, it might be desirable in the future to also defer computation
of polymorphic proofs whose constraints have been explicited in the type.
It is not clear when this is going to be implemented. Nonetheless, the
current check is not too drastic as it only prevents monomorphic side-effects
to appear inside polymorphic opaque definitions. The only way I know of to
trigger such a situation is to generate a scheme in a proof, as even abstract
is actually preserving the polymorphism status of the surrounding proof. It
would be possible to work around such rare instances anyways.

As for internal constraints generated by a potentially deferred polymorphic
body, it is easy to check that they are a subset of the exported ones at a
higher level inside the future computation and fail there.

So in practice this patch is not too restrictive and it highlights a rather
strong invariant of the kernel code.

1 files changed, 18 insertions, 10 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cbc4ee2ec..5f501bff1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -301,21 +301,29 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      let poly, univsctx = match c.const_entry_universes with
-      | Monomorphic_const_entry univs -> false, univs
-      | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs
-      in
-      let ctx = Univ.ContextSet.union univsctx ctx in
       let body, ctx, _ = match trust with
       | Pure -> body, ctx, []
       | SideEffects _ -> inline_side_effects env body ctx side_eff
       in
-      let env = push_context_set ~strict:(not poly) ctx env in
-      let ctx = if poly
-        then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
-        else Monomorphic_const_entry ctx
+      let env, usubst, univs = match c.const_entry_universes with
+      | Monomorphic_const_entry univs ->
+        let ctx = Univ.ContextSet.union univs ctx in
+        let env = push_context_set ~strict:true ctx env in
+        env, Univ.empty_level_subst, Monomorphic_const ctx
+      | Polymorphic_const_entry uctx ->
+        (** Ensure not to generate internal constraints in polymorphic mode.
+            The only way for this to happen would be that either the body
+            contained deferred universes, or that it contains monomorphic
+            side-effects. The first property is ruled out by upper layers,
+            and the second one is ensured by the fact we currently
+            unconditionally export side-effects from polymorphic definitions,
+            i.e. [trust] is always [Pure]. *)
+        let () = assert (Univ.ContextSet.is_empty ctx) in
+        let env = push_context ~strict:false uctx env in
+        let sbst, auctx = Univ.abstract_universes uctx in
+        let sbst = Univ.make_instance_subst sbst in
+        env, sbst, Polymorphic_const auctx
       in
-      let usubst, univs = abstract_constant_universes ctx in
       let j = infer env body in
       let typ = match typ with
         | None ->