Deprecate the nonuniform attribute

dev/ci/user-overlays/17716-proux01-deprecate_nonuniform.sh

@@ -0,0 +1,3 @@
+overlay elpi https://github.com/proux01/coq-elpi coq_17716 17716
+
+overlay mtac2 https://github.com/proux01/Mtac2 coq_17716 17716

doc/changelog/08-vernac-commands-and-options/17716-deprecate_nonuniform.rst

@@ -0,0 +1,5 @@
+- **Deprecated:**
+  the :attr:`nonuniform` attribute,
+  now subsumed by :attr:`warnings` with "-uniform-inheritance"
+  (`#17716 <https://github.com/coq/coq/pull/17716>`_,
+  by Pierre Roux).

doc/sphinx/addendum/implicit-coercions.rst

@@ -171,6 +171,10 @@ Coercion Classes
 
      Silence the non uniform inheritance warning.
 
+     .. deprecated:: 8.18
+
+        Use the :attr:`warnings` attribute instead with "-uniform-inheritance".
+
   .. exn:: @qualid not declared.
 
      :token:`qualid` is not defined globally.
@@ -209,7 +213,7 @@ Coercion Classes
 
      The :ref:`test for ambiguous coercion paths <ambiguous-paths>`
      may yield false positives involving the coercion :token:`qualid`.
-     Use the :attr:`nonuniform` attribute to silence this warning.
+     Use the :attr:`warnings` attribute with "-uniform-inheritance" to silence this warning.
 
   .. warn:: New coercion path ... is ambiguous with existing ...
 

test-suite/output/coercions_nonuniform.out

@@ -4,7 +4,3 @@ Warning: f does not respect the uniform inheritance condition.
 File "./output/coercions_nonuniform.v", line 55, characters 0-17:
 Warning: f' does not respect the uniform inheritance condition.
 [uniform-inheritance,coercions,default]
-File "./output/coercions_nonuniform.v", line 71, characters 7-17:
-The command has indeed failed with message:
-This command does not support this attribute: nonuniform.
-[unsupported-attributes,parsing,default]

test-suite/output/coercions_nonuniform.v

@@ -30,7 +30,7 @@ Parameter D : Type.
 Parameter f : forall (b : bool) (n : nat), C n b -> D.
 
 (* uniform inheritance not satisfied but attribute, no warning *)
-#[nonuniform] Coercion f : C >-> D.
+#[warning="-uniform-inheritance"] Coercion f : C >-> D.
 
 End Test2.
 
@@ -63,9 +63,6 @@ Parameter D : Type.
 Parameter f : forall (b : bool) (n : nat), C n b -> D.
 
 (* uniform inheritance not satisfied but attribute, no warning *)
-#[nonuniform] Coercion f' := f.
+#[warning="-uniform-inheritance"] Coercion f' := f.
 
 End Test5.
-
-(* Check that attribute is not supported for non coercion definitions *)
-Fail #[nonuniform] Definition f := id.

vernac/comAssumption.ml

@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ univs imps impl {CAst.v=name} =
   let () =
     if is_coe = Vernacexpr.AddCoercion then
       ComCoercion.try_add_new_coercion
-        r ~local:true ~poly:false ~nonuniform:false ~reversible:true in
+        r ~local:true ~poly:false ~reversible:true in
   ()
 
 let instance_of_univ_entry = function
@@ -59,7 +59,7 @@ let declare_axiom is_coe ~poly ~local ~kind ?deprecation typ (univs, ubinders) i
   let () =
     if is_coe = Vernacexpr.AddCoercion then
       ComCoercion.try_add_new_coercion
-        gr ~local ~poly ~nonuniform:false ~reversible:true in
+        gr ~local ~poly ~reversible:true in
   let inst = instance_of_univ_entry univs in
   (gr,inst)
 

vernac/comCoercion.ml

@@ -301,7 +301,7 @@ let warn_uniform_inheritance =
           Printer.pr_global g ++
             strbrk" does not respect the uniform inheritance condition.")
 
-let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target isid : unit =
+let add_new_coercion_core coef stre poly ~reversible source target isid : unit =
   check_source source;
   let env = Global.env () in
   let t, _ = Typeops.type_of_global_in_context env coef in
@@ -316,7 +316,7 @@ let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target i
       raise (CoercionError (NoSource source))
   in
   check_source (Some cls);
-  if not (nonuniform || uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *)
+  if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *)
                           ctx lvs) then
     warn_uniform_inheritance coef;
   let clt =
@@ -335,45 +335,44 @@ let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target i
   let params = List.length (Context.Rel.instance_list EConstr.mkRel 0 ctx) in
   declare_coercion coef t ~local ~reversible ~isid ~src:cls ~target:clt ~params ()
 
-
-let try_add_new_coercion_core ref ~local c ~nonuniform ~reversible d e f =
-  try add_new_coercion_core ref (loc_of_bool local) c ~nonuniform ~reversible d e f
+let try_add_new_coercion_core ref ~local c ~reversible d e f =
+  try add_new_coercion_core ref (loc_of_bool local) c ~reversible d e f
   with CoercionError e ->
       user_err
         (explain_coercion_error ref e ++ str ".")
 
-let try_add_new_coercion ref ~local ~poly ~nonuniform ~reversible =
-  try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible None None false
+let try_add_new_coercion ref ~local ~poly ~reversible =
+  try_add_new_coercion_core ref ~local poly ~reversible None None false
 
-let try_add_new_coercion_subclass cl ~local ~poly ~nonuniform ~reversible =
+let try_add_new_coercion_subclass cl ~local ~poly ~reversible =
   let coe_ref = build_id_coercion None cl poly in
-  try_add_new_coercion_core coe_ref ~local poly ~nonuniform ~reversible (Some cl) None true
+  try_add_new_coercion_core coe_ref ~local poly ~reversible (Some cl) None true
 
-let try_add_new_coercion_with_target ref ~local ~poly ~nonuniform ~reversible ~source ~target =
-  try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible
+let try_add_new_coercion_with_target ref ~local ~poly ~reversible ~source ~target =
+  try_add_new_coercion_core ref ~local poly ~reversible
     (Some source) (Some target) false
 
 let try_add_new_identity_coercion id ~local ~poly ~source ~target =
   let ref = build_id_coercion (Some id) source poly in
-  try_add_new_coercion_core ref ~local poly ~nonuniform:false ~reversible:true
+  try_add_new_coercion_core ref ~local poly ~reversible:true
     (Some source) (Some target) true
 
-let try_add_new_coercion_with_source ref ~local ~poly ~nonuniform ~reversible ~source =
-  try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible (Some source) None false
+let try_add_new_coercion_with_source ref ~local ~poly ~reversible ~source =
+  try_add_new_coercion_core ref ~local poly ~reversible (Some source) None false
 
-let add_coercion_hook poly nonuniform reversible { Declare.Hook.S.scope; dref; _ } =
+let add_coercion_hook poly reversible { Declare.Hook.S.scope; dref; _ } =
   let open Locality in
   let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
-  let () = try_add_new_coercion dref ~local ~poly ~nonuniform ~reversible in
+  let () = try_add_new_coercion dref ~local ~poly ~reversible in
   let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook ~poly ~nonuniform ~reversible =
-  Declare.Hook.make (add_coercion_hook poly nonuniform reversible)
+let add_coercion_hook ~poly ~reversible =
+  Declare.Hook.make (add_coercion_hook poly reversible)
 
 let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
   let open Locality in
@@ -383,7 +382,7 @@ let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
   | Global ImportDefaultBehavior -> false
   in
   let cl = class_of_global dref in
-  try_add_new_coercion_subclass cl ~local:stre ~poly ~nonuniform:false
+  try_add_new_coercion_subclass cl ~local:stre ~poly
 
 let nonuniform = Attributes.bool_attribute ~name:"nonuniform"
 

vernac/comCoercion.mli

@@ -19,7 +19,6 @@ val try_add_new_coercion_with_target
   :  GlobRef.t
   -> local:bool
   -> poly:bool
-  -> nonuniform:bool
   -> reversible:bool
   -> source:cl_typ
   -> target:cl_typ
@@ -28,21 +27,19 @@ val try_add_new_coercion_with_target
 (** [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
 val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool ->
-  nonuniform:bool ->
   reversible:bool -> unit
 
 (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
    transparent constant which unfolds to some class [tg]; it declares
    an identity coercion from [cst] to [tg], named something like
    ["Id_cst_tg"] *)
 val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool ->
-  nonuniform:bool ->
   reversible:bool -> unit
 
 (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
 val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
-  poly:bool -> nonuniform:bool -> reversible:bool -> source:cl_typ -> unit
+  poly:bool -> reversible:bool -> source:cl_typ -> unit
 
 (** [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
@@ -52,14 +49,14 @@ val try_add_new_identity_coercion
   -> local:bool
   -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : poly:bool -> nonuniform:bool -> reversible:bool -> Declare.Hook.t
+val add_coercion_hook : poly:bool -> reversible:bool -> Declare.Hook.t
 
 val add_subclass_hook : poly:bool -> reversible:bool -> Declare.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
 
 (** Attribute to silence warning for coercions that don't satisfy
-   the uniform inheritance condition. *)
+   the uniform inheritance condition. (deprecated in 8.18) *)
 val nonuniform : bool option Attributes.attribute
 
 val change_reverse : GlobRef.t -> reversible:bool -> unit

vernac/comInductive.ml

@@ -811,7 +811,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) where_notations;
   (* Declare the coercions *)
-  List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~nonuniform:false ~reversible:true) coercions
+  List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~reversible:true) coercions
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name

vernac/record.ml

@@ -340,7 +340,7 @@ let declare_proj_coercion_instance ~flags ref from ~poly ~with_coercion =
   if with_coercion && flags.Data.pf_coercion then begin
     let cl = ComCoercion.class_of_global from in
     let local = flags.Data.pf_locality = Goptions.OptLocal in
-    ComCoercion.try_add_new_coercion_with_source ref ~local ~poly ~nonuniform:false ~reversible:flags.Data.pf_reversible ~source:cl
+    ComCoercion.try_add_new_coercion_with_source ref ~local ~poly ~reversible:flags.Data.pf_reversible ~source:cl
   end;
   if flags.Data.pf_instance then begin
     let env = Global.env () in
@@ -803,7 +803,7 @@ let declare_structure { Record_decl.mie; primitive_proj; impls; globnames; globa
     let cstr = (rsp, 1) in
     let projections = declare_projections rsp (projunivs,ubinders) ~kind:projections_kind inhabitant_id proj_flags implfs fields in
     let build = GlobRef.ConstructRef cstr in
-    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly ~nonuniform:false ~reversible:true in
+    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly ~reversible:true in
     let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
     GlobRef.IndRef rsp

vernac/vernacentries.ml

@@ -60,7 +60,6 @@ module DefAttributes = struct
     canonical_instance : bool;
     typing_flags : Declarations.typing_flags option;
     using : Vernacexpr.section_subset_expr option;
-    nonuniform : bool;
     reversible : bool;
     clearbody: bool option;
   }
@@ -71,23 +70,21 @@ module DefAttributes = struct
   let clearbody = bool_attribute ~name:"clearbody"
 
   let parse ?(coercion=false) ?(discharge=NoDischarge) f =
-    let nonuniform = if coercion then ComCoercion.nonuniform else return None in
     let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in
-    let ((((((((locality, deprecated), polymorphic), program),
-         canonical_instance), typing_flags), using), nonuniform),
+    let (((((((locality, deprecated), polymorphic), program),
+         canonical_instance), typing_flags), using),
          reversible), clearbody =
       parse (locality ++ deprecation ++ polymorphic ++ program ++
-             canonical_instance ++ typing_flags ++ using ++ nonuniform ++
+             canonical_instance ++ typing_flags ++ using ++
              reversible ++ clearbody)
         f
     in
     let using = Option.map Proof_using.using_from_string using in
     let reversible = Option.default true reversible in
-    let nonuniform = Option.default false nonuniform in
     let () = if Option.has_some clearbody && not (Lib.sections_are_opened())
       then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.")
     in
-    { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using; nonuniform; reversible; clearbody }
+    { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using; reversible; clearbody }
 end
 
 let with_def_attributes ?coercion ?discharge ~atts f =
@@ -646,9 +643,9 @@ let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ~d
   (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *)
   |> vernac_set_used_variables_opt ?using
 
-let vernac_definition_hook ~canonical_instance ~local ~poly ~nonuniform ~reversible = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~local ~poly ~reversible = let open Decls in function
 | Coercion ->
-  Some (ComCoercion.add_coercion_hook ~poly ~nonuniform ~reversible)
+  Some (ComCoercion.add_coercion_hook ~poly ~reversible)
 | CanonicalStructure ->
   Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
@@ -680,7 +677,7 @@ let vernac_definition_name lid local =
 let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~nonuniform:atts.nonuniform ~reversible:atts.reversible kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~reversible:atts.reversible kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let typing_flags = atts.typing_flags in
@@ -692,7 +689,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
 let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let scope = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind ~nonuniform:atts.nonuniform ~reversible:atts.reversible in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind ~reversible:atts.reversible in
   let program_mode = atts.program in
   let typing_flags = atts.typing_flags in
   let name = vernac_definition_name lid scope in
@@ -1407,14 +1404,13 @@ let vernac_coercion ~atts ref qidst =
   let ref' = smart_global ref in
   match qidst with
   | Some (qids, qidt) ->
-     let ((local, poly), nonuniform), reversible =
-       Attributes.parse Notations.(locality ++ polymorphic ++ ComCoercion.nonuniform ++ reversible) atts in
+     let (local, poly), reversible =
+       Attributes.parse Notations.(locality ++ polymorphic ++ reversible) atts in
      let local = enforce_locality local in
-     let nonuniform = Option.default false nonuniform in
      let reversible = Option.default false reversible in
      let target = cl_of_qualid qidt in
      let source = cl_of_qualid qids in
-     ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~nonuniform ~reversible
+     ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~reversible
        ~source ~target;
      Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
   | None ->

vernac/vernacinterp.ml

@@ -104,6 +104,12 @@ let interp_control_entry ~loc (f : control_entry) ~st
   | ControlRedirect s ->
     Topfmt.with_output_to_file s (fun () -> fn ~st) ()
 
+let deprecated_nonuniform =
+  CWarnings.create ~name:"deprecated-nonuniform-attribute"
+    ~category:Deprecation.Version.v8_18
+    Pp.(fun () -> strbrk "Attribute '#[nonuniform]' is deprecated, \
+                          use '#[warning=\"-uniform-inheritance\"]' instead.")
+
 let warnings_att =
   Attributes.attribute_of_list [
     "warnings", Attributes.payload_parser ~cat:(^) ~name:"warnings";
@@ -112,6 +118,12 @@ let warnings_att =
 
 let with_generic_atts atts f =
   let atts, warnings = Attributes.parse_with_extra warnings_att atts in
+  let atts, nonuniform = Attributes.parse_with_extra ComCoercion.nonuniform atts in
+  let warnings =
+    let () = if nonuniform <> None then deprecated_nonuniform () in
+    if nonuniform <> Some true then warnings else
+      let ui = "-uniform-inheritance" in
+      Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in
   match warnings with
   | None -> f ~atts
   | Some warnings -> CWarnings.with_warn warnings (fun () -> f ~atts) ()