Univ declarations can have extensible qualities (internally)

Not supported in syntax as due to collapsing qualities any quality we
see must be named, but side effects use default_univ_decl which must
allow the named qualities from the surrounding proof.

Fix #19072

engine/uState.ml

@@ -762,6 +762,7 @@ let pr_uctx_qvar uctx l = pr_uctx_qvar_names uctx.names l
 
 type ('a, 'b, 'c) gen_universe_decl = {
   univdecl_qualities : 'a;
+  univdecl_extensible_qualities : bool;
   univdecl_instance : 'b; (* Declared universes *)
   univdecl_extensible_instance : bool; (* Can new universes be added *)
   univdecl_constraints : 'c; (* Declared constraints *)
@@ -772,6 +773,10 @@ type universe_decl =
 
 let default_univ_decl =
   { univdecl_qualities = [];
+    (* in practice non named qualities will get collapsed for toplevel definitions,
+       but side effects see named qualities from the surrounding definitions
+       while using default_univ_decl *)
+    univdecl_extensible_qualities = true;
     univdecl_instance = [];
     univdecl_extensible_instance = true;
     univdecl_constraints = Constraints.empty;
@@ -825,9 +830,10 @@ let universe_context_inst decl qvars levels names =
   let leftqs = List.fold_left (fun acc l -> QVar.Set.remove l acc) qvars decl.univdecl_qualities in
   let leftus = List.fold_left (fun acc l -> Level.Set.remove l acc) levels decl.univdecl_instance in
   let () =
+    let unboundqs = if decl.univdecl_extensible_qualities then QVar.Set.empty else leftqs in
     let unboundus = if decl.univdecl_extensible_instance then Level.Set.empty else leftus in
-    if not (QVar.Set.is_empty leftqs && Level.Set.is_empty unboundus)
-    then error_unbound_universes leftqs unboundus names
+    if not (QVar.Set.is_empty unboundqs && Level.Set.is_empty unboundus)
+    then error_unbound_universes unboundqs unboundus names
   in
   let leftqs = UContext.sort_qualities
       (Array.map_of_list (fun q -> Quality.QVar q) (QVar.Set.elements leftqs))
@@ -1179,9 +1185,10 @@ let universe_context_inst_decl decl qvars levels names =
   let leftqs = List.fold_left (fun acc l -> QVar.Set.remove l acc) qvars decl.univdecl_qualities in
   let leftus = List.fold_left (fun acc l -> Level.Set.remove l acc) levels decl.univdecl_instance in
   let () =
+    let unboundqs = if decl.univdecl_extensible_qualities then QVar.Set.empty else leftqs in
     let unboundus = if decl.univdecl_extensible_instance then Level.Set.empty else leftus in
-    if not (QVar.Set.is_empty leftqs && Level.Set.is_empty unboundus)
-    then error_unbound_universes leftqs unboundus names
+    if not (QVar.Set.is_empty unboundqs && Level.Set.is_empty unboundus)
+    then error_unbound_universes unboundqs unboundus names
   in
   let instq = Array.map_of_list (fun q -> Quality.QVar q) decl.univdecl_qualities in
   let instu = Array.of_list decl.univdecl_instance in

engine/uState.mli

@@ -220,6 +220,7 @@ val collapse_sort_variables : t -> t
 
 type ('a, 'b, 'c) gen_universe_decl = {
   univdecl_qualities : 'a;
+  univdecl_extensible_qualities : bool;
   univdecl_instance : 'b; (* Declared universes *)
   univdecl_extensible_instance : bool; (* Can new universes be added *)
   univdecl_constraints : 'c; (* Declared constraints *)

interp/constrintern.ml

@@ -2967,6 +2967,7 @@ let interp_univ_decl env decl =
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = {
     univdecl_qualities = qualities;
+    univdecl_extensible_qualities = decl.univdecl_extensible_qualities;
     univdecl_instance = instance;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
@@ -2992,6 +2993,7 @@ let interp_cumul_univ_decl env decl =
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = {
     univdecl_qualities = qualities;
+    univdecl_extensible_qualities = decl.univdecl_extensible_qualities;
     univdecl_instance = instance;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;

test-suite/bugs/bug_19072.v

@@ -0,0 +1,15 @@
+Set Universe Polymorphism.
+
+Definition demo@{srt|u |} : True.
+Proof.
+  abstract exact I.
+Defined.
+
+(* abstract doesn't restrict named qualities and universes
+   (debatable behaviour but that's what it does currently) *)
+Check demo@{Type|Set}.
+
+Definition baz@{q|u|} (A:Type@{q|u}) (x:A) : A.
+Proof.
+  abstract exact x.
+Defined.

vernac/comRewriteRule.ml

@@ -398,6 +398,7 @@ let interp_rule (udecl, lhs, rhs: Constrexpr.universe_decl_expr option * _ * _)
     in
     let decl = {
       univdecl_qualities = qualities;
+      univdecl_extensible_qualities = udecl.univdecl_extensible_qualities;
       univdecl_instance = instance;
       univdecl_extensible_instance = udecl.univdecl_extensible_instance;
       univdecl_constraints = cstrs;

vernac/g_vernac.mlg

@@ -353,6 +353,7 @@ GRAMMAR EXTEND Gram
          ->
          { let open UState in
          { univdecl_qualities = l0;
+           univdecl_extensible_qualities = false;
            univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;
@@ -361,7 +362,8 @@ GRAMMAR EXTEND Gram
          cs = univ_decl_constraints
          ->
          { let open UState in
-         { univdecl_qualities = []; (* TODO *)
+         { univdecl_qualities = [];
+           univdecl_extensible_qualities = false;
            univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;
@@ -388,6 +390,7 @@ GRAMMAR EXTEND Gram
          ->
          { let open UState in
          { univdecl_qualities = l0;
+           univdecl_extensible_qualities = false;
            univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;
@@ -398,6 +401,7 @@ GRAMMAR EXTEND Gram
          ->
          { let open UState in
          { univdecl_qualities = [];
+           univdecl_extensible_qualities = false;
            univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;