Merge PR #6483: Strong invariants in polymorphic definitions

4 files changed, 28 insertions, 17 deletions

diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
new file mode 100644
index 000000000..78789a6fc
--- /dev/null
+++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then
+    HoTT_CI_BRANCH=check-poly-effects
+    HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git
+fi
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 ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 167d6bda0..d04bdb652 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -343,16 +343,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
     if poly || now then
       let make_body t (c, eff) =
         let body = c in
-	let typ =
-	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
-	    nf t
-	  else t
+        let allow_deferred =
+          not poly && (keep_body_ucst_separate ||
+          not (Safe_typing.empty_private_constants = eff))
         in
+        let typ = if allow_deferred then t else nf t in
         let env = Global.env () in
         let used_univs_body = Univops.universes_of_constr env body in
         let used_univs_typ = Univops.universes_of_constr env typ in
-        if keep_body_ucst_separate ||
-           not (Safe_typing.empty_private_constants = eff) then
+        if allow_deferred then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
index b736b734f..aa8da5336 100644
--- a/test-suite/success/abstract_poly.v
+++ b/test-suite/success/abstract_poly.v
@@ -17,4 +17,4 @@ intros m n P e p.
 abstract (rewrite e in p; exact p).
 Defined.
 
-Check bar_subproof@{Set Set Set}.
+Check bar_subproof@{Set Set}.