Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)

14 files changed, 102 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index 46266a1bd0..1bf0e0edd4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -221,6 +221,12 @@ Tools
   and `print-pretty-single-time-diff` now correctly label the "before" and
   "after" columns, rather than swapping them.
 
+Kernel
+
+- The kernel does not tolerate capture of global universes by
+  polymorphic universe binders, fixing a soundness break (triggered
+  only through custom plugins)
+
 Changes from 8.8.0 to 8.8.1
 ===========================
 
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 6166d24b70..8d78559c0d 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -109,6 +109,16 @@ Universes
   GH issue number: none
   risk: unlikely to be activated by chance
 
+  component: universe polymorphism
+  summary: universe polymorphism can capture global universes
+  impacted released versions: V8.5 to V8.8
+  impacted coqchk versions: V8.5 to current (NOT FIXED)
+  fixed in: 2385b5c1ef
+  found by: Gaëtan Gilbert
+  exploit: test-suite/misc/poly-capture-global-univs
+  GH issue number: #8341
+  risk: unlikely to be activated by chance (requires a plugin)
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 62c14f6f07..3bfcaa7f52 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -365,8 +365,7 @@ let push_constraints_to_env (_,univs) env =
 
 let add_universes strict ctx g =
   let g = Array.fold_left
-	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun g v -> UGraph.add_universe v strict g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
@@ -376,6 +375,7 @@ let push_context ?(strict=false) ctx env =
 
 let add_universes_set strict ctx g =
   let g = Univ.LSet.fold
+            (* Be lenient, module typing reintroduces universes and constraints due to includes *)
 	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f79e5270a2..7abf8027bd 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,8 +234,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
     let instance_other = Instance.of_array new_levels in
     let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env = Environ.push_context uctx env_ar in
-    let env = Environ.push_context uctx_other env in
+    let env = Environ.push_context uctx_other env_ar in
     let subtyp_constraints =
       CumulativityInfo.leq_constraints cumi
         (UContext.instance uctx) instance_other
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43351737e5..f59e07098b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -256,6 +256,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain body (fun ((body,uctx),side_eff) ->
+          (* don't redeclare universes which are declared for the type *)
+          let uctx = Univ.ContextSet.diff uctx univs in
           let j, uctx = match trust with
           | Pure ->
             let env = push_context_set uctx env in
diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh
new file mode 100755
index 0000000000..e066ac039b
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/poly-capture-global-univs/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cmxs
+
+if make; then
+    >&2 echo 'Should have failed!'
+    exit 1
+fi
diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore
new file mode 100644
index 0000000000..f5a6d22b8e
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/.gitignore
@@ -0,0 +1 @@
+/Makefile*
diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject
new file mode 100644
index 0000000000..70ec246062
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/_CoqProject
@@ -0,0 +1,9 @@
+-Q theories Evil
+-I src
+
+src/evil.ml4
+src/evilImpl.ml
+src/evilImpl.mli
+src/evil_plugin.mlpack
+theories/evil.v
+
diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4
new file mode 100644
index 0000000000..565e979aaa
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evil.ml4
@@ -0,0 +1,9 @@
+
+open Stdarg
+open EvilImpl
+
+DECLARE PLUGIN "evil_plugin"
+
+VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF
+| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ]
+END
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
new file mode 100644
index 0000000000..6d8ce7c5d7
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -0,0 +1,22 @@
+open Names
+
+let evil t f =
+  let open Univ in
+  let open Entries in
+  let open Decl_kinds in
+  let open Constr in
+  let k = IsDefinition Definition in
+  let u = Level.var 0 in
+  let tu = mkType (Universe.make u) in
+  let te = Declare.definition_entry
+      ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu
+  in
+  let tc = Declare.declare_constant t (DefinitionEntry te, k) in
+  let tc = mkConst tc in
+
+  let fe = Declare.definition_entry
+      ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~types:(Term.mkArrow tc tu)
+      (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
+  in
+  ignore (Declare.declare_constant f (DefinitionEntry fe, k))
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli
new file mode 100644
index 0000000000..97c7e3dadd
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.mli
@@ -0,0 +1,2 @@
+
+val evil : Names.Id.t -> Names.Id.t -> unit
diff --git a/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..0093328a40
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evil_plugin.mlpack
@@ -0,0 +1,2 @@
+EvilImpl
+Evil
diff --git a/test-suite/misc/poly-capture-global-univs/theories/evil.v b/test-suite/misc/poly-capture-global-univs/theories/evil.v
new file mode 100644
index 0000000000..7fd98c2773
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/theories/evil.v
@@ -0,0 +1,13 @@
+
+Declare ML Module "evil_plugin".
+
+Evil T f. (* <- if this doesn't fail then the rest goes through *)
+
+Definition g : Type -> Set := f.
+
+Require Import Hurkens.
+
+Lemma absurd : False.
+Proof.
+  exact (TypeNeqSmallType.paradox (g Type) eq_refl).
+Qed.
diff --git a/vernac/record.ml b/vernac/record.ml
index d36586d062..7ab2b50764 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -487,10 +487,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
       let cst = Declare.declare_constant id
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-      let cstu = (cst, match univs with
-        | Polymorphic_const_entry univs -> Univ.UContext.instance univs
-        | Monomorphic_const_entry _ -> Univ.Instance.empty)
+      let inst, univs = match univs with
+        | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+        | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
       in
+      let cstu = (cst, inst) in
       let inst_type = appvectc (mkConstU cstu)
 			       (Termops.rel_vect 0 (List.length params)) in
       let proj_type =