UState: don't check for unbound qualities as it doesn't make sense

due to collapsing qualities any quality we see must be named

Fix #19072

(we still have a check in the functions used by rewrite rules, not
sure if it's correct there but probably doesn't matter)

engine/uState.ml

@@ -826,8 +826,10 @@ let universe_context_inst decl qvars levels names =
   let leftus = List.fold_left (fun acc l -> Level.Set.remove l acc) levels decl.univdecl_instance in
   let () =
     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
+    (* allow unbound qualities, cf #19072
+       collapsing ensured that we only get named qualities anyway *)
+    if not (Level.Set.is_empty unboundus)
+    then error_unbound_universes QVar.Set.empty unboundus names
   in
   let leftqs = UContext.sort_qualities
       (Array.map_of_list (fun q -> Quality.QVar q) (QVar.Set.elements leftqs))

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.