Loosen restrictions on mixing universe mono/polymorphism in sections

We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.

Every other combination is already correctly discharged by the kernel.

11 files changed, 206 insertions, 155 deletions

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1d0b732e7d..905068e316 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -507,17 +507,45 @@ underscore or by omitting the annotation to a polymorphic definition.
 Universe polymorphism and sections
 ----------------------------------
 
-The universe polymorphic or monomorphic status is
-attached to each individual section, and all term or universe declarations
-contained inside must respect it, as described below. It is possible to nest a
-polymorphic section inside a monomorphic one, but the converse is not allowed.
-
-:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support
-polymorphism. This means that the universe variables and their associated
-constraints are discharged polymorphically over definitions that use
-them. In other words, two definitions in the section sharing a common
-variable will both get parameterized by the universes produced by the
-variable declaration. This is in contrast to a “mononorphic” variable
-which introduces global universes and constraints, making the two
-definitions depend on the *same* global universes associated to the
-variable.
+:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and
+:cmd:`Constraint` in a section support polymorphism. This means that
+the universe variables and their associated constraints are discharged
+polymorphically over definitions that use them. In other words, two
+definitions in the section sharing a common variable will both get
+parameterized by the universes produced by the variable declaration.
+This is in contrast to a “mononorphic” variable which introduces
+global universes and constraints, making the two definitions depend on
+the *same* global universes associated to the variable.
+
+It is possible to mix universe polymorphism and monomorphism in
+sections, except in the following ways:
+
+- no monomorphic constraint may refer to a polymorphic universe:
+
+  .. coqtop:: all reset
+
+     Section Foo.
+
+       Polymorphic Universe i.
+       Fail Constraint i = i.
+
+  This includes constraints implictly declared by commands such as
+  :cmd:`Variable`, which may as a such need to be used with universe
+  polymorphism activated (locally by attribute or globally by option):
+
+  .. coqtop:: all
+
+     Fail Variable A : (Type@{i} : Type).
+     Polymorphic Variable A : (Type@{i} : Type).
+
+  (in the above example the anonymous :g:`Type` constrains polymorphic
+  universe :g:`i` to be strictly smaller.)
+
+- no monomorphic constant or inductive may be declared if polymorphic
+  universes or universe constraints are present.
+
+These restrictions are required in order to produce a sensible result
+when closing the section (the requirement on constants and inductives
+is stricter than the one on constraints, because constants and
+inductives are abstracted by *all* the section's polymorphic universes
+and constraints).
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index db16bd1e79..4268f0a602 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -334,8 +334,6 @@ type constraints_addition =
 
 let push_context_set poly cst senv =
   if Univ.ContextSet.is_empty cst then senv
-  else if Section.is_polymorphic senv.sections then
-    CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
   else
     let sections =
       if Section.is_empty senv.sections then senv.sections
@@ -947,13 +945,13 @@ let add_module l me inl senv =
 
 (** {6 Interactive sections *)
 
-let open_section ~poly senv =
+let open_section senv =
   let custom = {
     rev_env = senv.env;
     rev_univ = senv.univ;
     rev_objlabels = senv.objlabels;
   } in
-  let sections = Section.open_section ~poly ~custom senv.sections in
+  let sections = Section.open_section ~custom senv.sections in
   { senv with sections }
 
 let close_section senv =
@@ -962,7 +960,6 @@ let close_section senv =
   let env0 = senv.env in
   (* First phase: revert the declarations added in the section *)
   let sections, entries, cstrs, revert = Section.close_section sections0 in
-  let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in
   let rec pop_revstruct accu entries revstruct = match entries, revstruct with
   | [], revstruct -> accu, revstruct
   | _ :: _, [] ->
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d3ca642a89..d97d61a72f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -134,7 +134,7 @@ val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
 
 (** {6 Interactive section functions } *)
 
-val open_section : poly:bool -> safe_transformer0
+val open_section : safe_transformer0
 
 val close_section : safe_transformer0
 
diff --git a/kernel/section.ml b/kernel/section.ml
index 188249e77e..4a9b222798 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -14,49 +14,38 @@ open Univ
 
 module NamedDecl = Context.Named.Declaration
 
-type _ section_kind =
-| SecMono : [ `mono ] section_kind
-| SecPoly : [ `poly ] section_kind
-
-type (_, 'a) section_universes =
-| SecMonoUniv : 'a -> ([ `mono ], 'a) section_universes
-| SecPolyUniv : Name.t array * UContext.t -> ([ `poly ], 'a) section_universes
-
 type section_entry =
 | SecDefinition of Constant.t
 | SecInductive of MutInd.t
 
 type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
 
-type ('a, 'b) section = {
+type 'a section = {
   sec_context : int;
   (** Length of the named context suffix that has been introduced locally *)
-  sec_universes : ('a, ContextSet.t) section_universes;
+  sec_mono_universes : ContextSet.t;
+  sec_poly_universes : Name.t array * UContext.t;
   (** Universes local to the section *)
+  has_poly_univs : bool;
+  (** Are there polymorphic universes or constraints, including in previous sections. *)
   sec_entries : section_entry list;
   (** Definitions introduced in the section *)
-  sec_data : ('a, unit) section_universes entry_map;
+  sec_data : (Instance.t * AUContext.t) entry_map;
   (** Additional data synchronized with the section *)
-  sec_custom : 'b;
+  sec_custom : 'a;
 }
 
 (** Sections can be nested with the proviso that no monomorphic section can be
     opened inside a polymorphic one. The reverse is allowed. *)
-type 'a t = {
-  sec_poly : ([ `poly ], 'a) section list;
-  sec_mono : ([ `mono ], 'a) section list;
-}
+type 'a t = 'a section list
 
-let empty = {
-  sec_poly = [];
-  sec_mono = [];
-}
+let empty = []
 
-let is_empty s =
-  List.is_empty s.sec_poly && List.is_empty s.sec_mono
+let is_empty = List.is_empty
 
-let is_polymorphic s =
-  not (List.is_empty s.sec_poly)
+let has_poly_univs = function
+  | [] -> false
+  | sec :: _ -> sec.has_poly_univs
 
 let find_emap e (cmap, imap) = match e with
 | SecDefinition con -> Cmap.find con cmap
@@ -66,104 +55,80 @@ let add_emap e v (cmap, imap) = match e with
 | SecDefinition con -> (Cmap.add con v cmap, imap)
 | SecInductive ind -> (cmap, Mindmap.add ind v imap)
 
-type 'b on_sec = { on_sec : 'a. 'a section_kind -> ('a, 'b) section -> ('a, 'b) section }
-
-let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
-| [], [] -> CErrors.user_err (Pp.str "No opened section")
-| sec :: rem, _ ->
-  let sec_poly = f.on_sec SecPoly sec :: rem in
-  { sec_mono; sec_poly }
-| [], sec :: rem ->
-  let sec_mono = f.on_sec SecMono sec :: rem in
-  { sec_mono; sec_poly }
+let on_last_section f sections = match sections with
+| [] -> CErrors.user_err (Pp.str "No opened section")
+| sec :: rem -> f sec :: rem
 
-type ('r, 'b) with_sec = { with_sec : 'a. ('a section_kind * ('a, 'b) section) option -> 'r }
-
-let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
-| [], [] -> f.with_sec None
-| sec :: _, _ -> f.with_sec (Some (SecPoly, sec))
-| [], sec :: _ -> f.with_sec (Some (SecMono, sec))
+let with_last_section f sections = match sections with
+| [] -> f None
+| sec :: _ -> f (Some sec)
 
 let push_local s =
-  let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in
-  on_last_section { on_sec } s
+  let on_sec sec = { sec with sec_context = sec.sec_context + 1 } in
+  on_last_section on_sec s
 
 let push_context (nas, ctx) s =
-  let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with
-  | SecMono ->
-    CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
-  | SecPoly ->
-    let SecPolyUniv (snas, sctx) = sec.sec_universes in
-    let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in
-    { sec with sec_universes }
+    let on_sec sec =
+      if UContext.is_empty ctx then sec
+      else
+        let (snas, sctx) = sec.sec_poly_universes in
+        let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
+        { sec with sec_poly_universes; has_poly_univs = true }
+    in
+    on_last_section on_sec s
+
+let is_polymorphic_univ u s =
+  let check sec =
+    let (_, uctx) = sec.sec_poly_universes in
+    Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx))
   in
-  on_last_section { on_sec } s
+  List.exists check s
 
 let push_constraints uctx s =
-  let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with
-  | SecMono ->
-    let SecMonoUniv uctx' = sec.sec_universes in
-    let sec_universes = SecMonoUniv (ContextSet.union uctx uctx') in
-    { sec with sec_universes }
-  | SecPoly ->
-    CErrors.anomaly (Pp.str "Adding monomorphic constraints to polymorphic section")
+  let on_sec sec =
+    if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx)
+    then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
+    let uctx' = sec.sec_mono_universes in
+    let sec_mono_universes =  (ContextSet.union uctx uctx') in
+    { sec with sec_mono_universes }
   in
-  on_last_section { on_sec } s
-
-let open_section ~poly ~custom sections =
-  if poly then
-    let sec = {
-      sec_context = 0;
-      sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
-      sec_entries = [];
-      sec_data = (Cmap.empty, Mindmap.empty);
-      sec_custom = custom;
-    } in
-    { sections with sec_poly = sec :: sections.sec_poly }
-  else if List.is_empty sections.sec_poly then
-    let sec = {
-      sec_context = 0;
-      sec_universes = SecMonoUniv Univ.ContextSet.empty;
-      sec_entries = [];
-      sec_data = (Cmap.empty, Mindmap.empty);
-      sec_custom = custom;
-    } in
-    { sections with sec_mono = sec :: sections.sec_mono }
-  else
-    CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+  on_last_section on_sec s
+
+let open_section ~custom sections =
+  let sec = {
+    sec_context = 0;
+    sec_mono_universes = ContextSet.empty;
+    sec_poly_universes = ([||], UContext.empty);
+    has_poly_univs = has_poly_univs sections;
+    sec_entries = [];
+    sec_data = (Cmap.empty, Mindmap.empty);
+    sec_custom = custom;
+  } in
+  sec :: sections
 
 let close_section sections =
-  match sections.sec_poly, sections.sec_mono with
-  | sec :: psecs, _ ->
-    let sections = { sections with sec_poly = psecs } in
-    sections, sec.sec_entries, Univ.ContextSet.empty, sec.sec_custom
-  | [], sec :: msecs ->
-    let sections = { sections with sec_mono = msecs } in
-    let SecMonoUniv cstrs = sec.sec_universes in
-    sections, sec.sec_entries, cstrs, sec.sec_custom
-  | [], [] ->
+  match sections with
+  | sec :: sections ->
+    sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
+  | [] ->
     CErrors.user_err (Pp.str "No opened section.")
 
-let same_poly (type a) ~poly (knd : a section_kind) = match knd with
-| SecPoly -> poly
-| SecMono -> not poly
-
-let drop_global (type a) : (a, _) section_universes -> (a, unit) section_universes = function
-| SecMonoUniv _ -> SecMonoUniv ()
-| SecPolyUniv _ as u -> u
+let make_decl_univs (nas,uctx) = abstract_universes nas uctx
 
 let push_global ~poly e s =
   if is_empty s then s
+  else if has_poly_univs s && not poly
+  then CErrors.user_err
+      Pp.(str "Cannot add a universe monomorphic declaration when \
+               section polymorphic universes are present.")
   else
-    let on_sec knd sec =
-      if same_poly ~poly knd then { sec with
+    let on_sec sec =
+      { sec with
         sec_entries = e :: sec.sec_entries;
-        sec_data = add_emap e (drop_global sec.sec_universes) sec.sec_data;
-      } else
-        CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
-          monomorphic declarations in sections.")
+        sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
+      }
     in
-    on_last_section { on_sec } s
+    on_last_section on_sec s
 
 let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
 
@@ -171,8 +136,8 @@ let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s
 
 type abstr_info = {
   abstr_ctx : Constr.named_context;
-  abstr_subst : Univ.Instance.t;
-  abstr_uctx : Univ.AUContext.t;
+  abstr_subst : Instance.t;
+  abstr_uctx : AUContext.t;
 }
 
 let empty_segment = {
@@ -198,24 +163,19 @@ let extract_hyps sec vars hyps =
 let section_segment_of_entry vars e hyps sections =
   (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
     global *)
-  let with_sec (type a) (s : (a section_kind * (a, _) section) option) = match s with
+  let with_sec s = match s with
   | None ->
     CErrors.user_err (Pp.str "No opened section.")
-  | Some (knd, sec) ->
+  | Some sec ->
     let hyps = extract_hyps sec vars hyps in
-    let inst, auctx = match knd, find_emap e sec.sec_data with
-    | SecMono, SecMonoUniv () ->
-      Instance.empty, AUContext.empty
-    | SecPoly, SecPolyUniv (nas, ctx) ->
-      Univ.abstract_universes nas ctx
-    in
+    let inst, auctx = find_emap e sec.sec_data in
     {
       abstr_ctx = hyps;
       abstr_subst = inst;
       abstr_uctx = auctx;
     }
   in
-  with_last_section { with_sec } sections
+  with_last_section with_sec sections
 
 let segment_of_constant env con s =
   let body = Environ.lookup_constant con env in
@@ -237,18 +197,18 @@ let extract_worklist info =
 let replacement_context env s =
   let with_sec sec = match sec with
   | None -> CErrors.user_err (Pp.str "No opened section.")
-  | Some (_, sec) ->
+  | Some sec ->
     let cmap, imap = sec.sec_data in
     let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
     let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
     (cmap, imap)
   in
-  with_last_section { with_sec } s
+  with_last_section with_sec s
 
 let is_in_section env gr s =
   let with_sec sec = match sec with
   | None -> false
-  | Some (_, sec) ->
+  | Some sec ->
     let open GlobRef in
     match gr with
     | VarRef id ->
@@ -259,11 +219,4 @@ let is_in_section env gr s =
     | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
       Mindmap.mem ind (snd sec.sec_data)
   in
-  with_last_section { with_sec } s
-
-let is_polymorphic_univ u s =
-  let check sec =
-    let SecPolyUniv (_, uctx) = sec.sec_universes in
-    Array.mem u (Instance.to_array (UContext.instance uctx))
-  in
-  List.exists check s.sec_poly
+  with_last_section with_sec s
diff --git a/kernel/section.mli b/kernel/section.mli
index c1026a2980..fc3ac141e4 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -21,16 +21,13 @@ val empty : 'a t
 val is_empty : 'a t -> bool
 (** Checks whether there is no opened section *)
 
-val is_polymorphic : 'a t -> bool
-(** Checks whether last opened section is polymorphic *)
-
 (** {6 Manipulating sections} *)
 
 type section_entry =
 | SecDefinition of Constant.t
 | SecInductive of MutInd.t
 
-val open_section : poly:bool -> custom:'a -> 'a t -> 'a t
+val open_section : custom:'a -> 'a t -> 'a t
 (** Open a new section with the provided universe polymorphic status. Sections
     can be nested, with the proviso that polymorphic sections cannot appear
     inside a monomorphic one. A custom data can be attached to this section,
diff --git a/library/global.ml b/library/global.ml
index 315a147d2c..c4685370d1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -109,7 +109,7 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
-let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let open_section () = globalize0 Safe_typing.open_section
 let close_section fs = globalize0_with_summary fs Safe_typing.close_section
 
 let start_module id = globalize (Safe_typing.start_module (i2l id))
diff --git a/library/global.mli b/library/global.mli
index 26ccb90271..c45bf65d84 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -73,7 +73,7 @@ val add_include :
 
 (** Sections *)
 
-val open_section : poly:bool -> unit
+val open_section : unit -> unit
 (** [poly] is true when the section should be universe polymorphic *)
 
 val close_section : Summary.frozen -> unit
diff --git a/library/lib.ml b/library/lib.ml
index 1c6f82e8a6..991e23eb3a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -464,8 +464,8 @@ let section_instance = let open GlobRef in function
 
 (*************)
 (* Sections. *)
-let open_section ~poly id =
-  let () = Global.open_section ~poly in
+let open_section id =
+  let () = Global.open_section () in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
diff --git a/library/lib.mli b/library/lib.mli
index 5ce601f2d3..d3315b0f2e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -147,7 +147,7 @@ val library_part :  GlobRef.t -> DirPath.t
 
 (** {6 Sections } *)
 
-val open_section : poly:bool -> Id.t -> unit
+val open_section : Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
diff --git a/test-suite/success/section_poly.v b/test-suite/success/section_poly.v
new file mode 100644
index 0000000000..1e2201f2de
--- /dev/null
+++ b/test-suite/success/section_poly.v
@@ -0,0 +1,74 @@
+
+
+Section Foo.
+
+  Variable X : Type.
+
+  Polymorphic Section Bar.
+
+  Variable A : Type.
+
+  Definition id (a:A) := a.
+
+End Bar.
+Check id@{_}.
+End Foo.
+Check id@{_}.
+
+Polymorphic Section Foo.
+Variable A : Type.
+Section Bar.
+  Variable B : Type.
+
+  Inductive prod := Prod : A -> B -> prod.
+End Bar.
+Check prod@{_}.
+End Foo.
+Check prod@{_ _}.
+
+Section Foo.
+
+  Universe K.
+  Inductive bla := Bla : Type@{K} -> bla.
+
+  Polymorphic Definition bli@{j} := Type@{j} -> bla.
+
+  Definition bloo := bli@{_}.
+
+  Polymorphic Universe i.
+
+  Fail Definition x := Type.
+  Fail Inductive x : Type := .
+  Polymorphic Definition x := Type.
+  Polymorphic Inductive y : x := .
+
+  Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *)
+
+  Fail Variable B : (y : Type@{i}).
+  (* not allowed: mono constraint (about a fresh univ for y) regarding
+  poly univ i *)
+
+  Polymorphic Variable B : Type. (* new polymorphic stuff always OK *)
+
+  Variable C : Type@{i}. (* no new univs so no problems *)
+
+  Polymorphic Definition thing := bloo -> y -> A -> B.
+
+End Foo.
+Check bli@{_}.
+Check bloo@{}.
+
+Check thing@{_ _ _}.
+
+Section Foo.
+
+  Polymorphic Universes i k.
+  Universe j.
+  Fail Constraint i < j.
+  Fail Constraint i < k.
+
+  (* referring to mono univs in poly constraints is OK. *)
+  Polymorphic Constraint i < j. Polymorphic Constraint j < k.
+
+  Polymorphic Definition foo := Type@{j}.
+End Foo.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 43b58d6d4b..c3be57eec8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -980,7 +980,9 @@ let vernac_include l =
 
 let vernac_begin_section ~poly ({v=id} as lid) =
   Dumpglob.dump_definition lid true "sec";
-  Lib.open_section ~poly id;
+  Lib.open_section id;
+  (* If there was no polymorphism attribute this just sets the option
+     to its current value ie noop. *)
   set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly
 
 let vernac_end_section {CAst.loc} =