Add a nonuniform attribute silencing warning on coercions

dev/ci/user-overlays/15853-proux01-nonuniform_attr.sh

@@ -0,0 +1,2 @@
+overlay elpi https://github.com/proux01/coq-elpi coq_15853 15853
+overlay mtac2 https://github.com/proux01/Mtac2 coq_15853 15853

doc/changelog/07-vernac-commands-and-options/15853-nonuniform_attr.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  the :attr:`nonuniform` boolean attribute that silences the
+  non-uniform-inheritance warning when user needs to declare such a
+  coercion on purpose
+  (`#15853 <https://github.com/coq/coq/pull/15853>`_,
+  by Pierre Roux, reviewed by Gaëtan Gilbert and Jim Fehrle).

doc/sphinx/addendum/implicit-coercions.rst

@@ -122,6 +122,14 @@ Declaring Coercions
   and then declares :token:`ident` as a coercion between it source and its target.
   Both forms support the :attr:`local` attribute, which makes the coercion local to the current section.
 
+  This command supports the :attr:`local` and :attr:`global` attributes
+  (described :ref:`here <set_unset_scope_qualifiers>`) as well as the
+  :attr:`nonuniform` attribute.
+
+  .. attr:: nonuniform
+
+     Silence the non uniform inheritance warning.
+
   .. exn:: @qualid not declared.
      :undocumented:
 
@@ -147,6 +155,7 @@ Declaring Coercions
 
      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.
 
   .. warn:: New coercion path ... is ambiguous with existing ...
 

test-suite/output/coercions_nonuniform.out

@@ -0,0 +1,10 @@
+File "./output/coercions_nonuniform.v", line 22, characters 0-21:
+Warning: f does not respect the uniform inheritance condition.
+[uniform-inheritance,typechecker]
+File "./output/coercions_nonuniform.v", line 55, characters 0-17:
+Warning: f' does not respect the uniform inheritance condition.
+[uniform-inheritance,typechecker]
+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]

test-suite/output/coercions_nonuniform.v

@@ -0,0 +1,71 @@
+(* Test the nonuniform attribute to silence warnings on coercions
+   not satisfying the non uniform inheritance condition. *)
+
+Module Test0.
+
+Parameter C : nat -> bool -> Type.
+Parameter D : Type.
+Parameter f : forall (n : nat) (b : bool), C n b -> D.
+
+(* uniform inheritance satisfied, no warning *)
+Coercion f : C >-> D.
+
+End Test0.
+
+Module Test1.
+
+Parameter C : nat -> bool -> Type.
+Parameter D : Type.
+Parameter f : forall (b : bool) (n : nat), C n b -> D.
+
+(* uniform inheritance not satisfied, warning *)
+Coercion f : C >-> D.
+
+End Test1.
+
+Module Test2.
+
+Parameter C : nat -> bool -> Type.
+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.
+
+End Test2.
+
+Module Test3.
+
+Parameter C : nat -> bool -> Type.
+Parameter D : Type.
+Parameter f : forall (n : nat) (b : bool), C n b -> D.
+
+(* uniform inheritance satisfied, no warning *)
+Coercion f' := f.
+
+End Test3.
+
+Module Test4.
+
+Parameter C : nat -> bool -> Type.
+Parameter D : Type.
+Parameter f : forall (b : bool) (n : nat), C n b -> D.
+
+(* uniform inheritance not satisfied, warning *)
+Coercion f' := f.
+
+End Test4.
+
+Module Test5.
+
+Parameter C : nat -> bool -> Type.
+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.
+
+End Test5.
+
+(* Check that attribute is not supported for non coercion definitions *)
+Fail #[nonuniform] Definition f := id.

vernac/comAssumption.ml

@@ -29,7 +29,7 @@ let declare_variable is_coe ~kind typ univs imps impl {CAst.v=name} =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None Hints.Local r in
-  let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in
+  let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false ~nonuniform:false in
   ()
 
 let instance_of_univ_entry = function
@@ -62,7 +62,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, ubinders) imps nl {CAst.
     | Locality.ImportNeedQualified -> true
     | Locality.ImportDefaultBehavior -> false
   in
-  let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
+  let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly ~nonuniform:false 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 source target isid : unit =
+let add_new_coercion_core coef stre poly ~nonuniform source target isid : unit =
   check_source source;
   let env = Global.env () in
   let t, _ = Typeops.type_of_global_in_context env coef in
@@ -316,8 +316,8 @@ let add_new_coercion_core coef stre poly source target isid : unit =
       raise (CoercionError (NoSource source))
   in
   check_source (Some cls);
-  if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *)
-                       ctx lvs) then
+  if not (nonuniform || uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *)
+                          ctx lvs) then
     warn_uniform_inheritance coef;
   let clt =
     try
@@ -336,8 +336,8 @@ let add_new_coercion_core coef stre poly source target isid : unit =
   declare_coercion coef t ~local ~isid ~src:cls ~target:clt ~params ()
 
 
-let try_add_new_coercion_core ref ~local c d e f =
-  try add_new_coercion_core ref (loc_of_bool local) c d e f
+let try_add_new_coercion_core ref ~local c ~nonuniform d e f =
+  try add_new_coercion_core ref (loc_of_bool local) c ~nonuniform d e f
   with CoercionError e ->
       user_err
         (explain_coercion_error ref e ++ str ".")
@@ -349,28 +349,32 @@ let try_add_new_coercion_subclass cl ~local ~poly =
   let coe_ref = build_id_coercion None cl poly in
   try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
 
-let try_add_new_coercion_with_target ref ~local ~poly ~source ~target =
-  try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
+let try_add_new_coercion_with_target ref ~local ~poly ~nonuniform
+      ~source ~target =
+  try_add_new_coercion_core ref ~local poly ~nonuniform
+    (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 (Some source) (Some target) true
+  try_add_new_coercion_core ref ~local poly ~nonuniform:false
+    (Some source) (Some target) true
 
-let try_add_new_coercion_with_source ref ~local ~poly ~source =
-  try_add_new_coercion_core ref ~local poly (Some source) None false
+let try_add_new_coercion_with_source ref ~local ~poly ~nonuniform ~source =
+  try_add_new_coercion_core ref ~local poly ~nonuniform (Some source) None false
 
-let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
+let add_coercion_hook poly nonuniform { 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 in
+  let () = try_add_new_coercion dref ~local ~poly ~nonuniform 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 = Declare.Hook.make (add_coercion_hook poly)
+let add_coercion_hook ~poly ~nonuniform =
+  Declare.Hook.make (add_coercion_hook poly nonuniform)
 
 let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
   let open Locality in
@@ -380,6 +384,8 @@ 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
+  try_add_new_coercion_subclass cl ~local:stre ~poly ~nonuniform:false
 
 let add_subclass_hook ~poly = Declare.Hook.make (add_subclass_hook ~poly)
+
+let nonuniform = Attributes.bool_attribute ~name:"nonuniform"

vernac/comCoercion.mli

@@ -19,24 +19,27 @@ val try_add_new_coercion_with_target
   :  GlobRef.t
   -> local:bool
   -> poly:bool
+  -> nonuniform:bool
   -> source:cl_typ
   -> target:cl_typ
   -> unit
 
 (** [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 -> unit
+val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool ->
+  nonuniform: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 -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool ->
+  nonuniform: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 -> source:cl_typ -> unit
+  poly:bool -> nonuniform: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
@@ -46,8 +49,12 @@ val try_add_new_identity_coercion
   -> local:bool
   -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : poly:bool -> Declare.Hook.t
+val add_coercion_hook : poly:bool -> nonuniform:bool -> Declare.Hook.t
 
 val add_subclass_hook : poly: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. *)
+val nonuniform : bool option Attributes.attribute

vernac/comInductive.ml

@@ -685,7 +685,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 ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
+  List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~nonuniform:false) coes
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name

vernac/record.ml

@@ -380,7 +380,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
   Impargs.maybe_declare_manual_implicits false refi impls;
   if flags.pf_subclass then begin
     let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
-    ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+    ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~nonuniform:false ~source:cl
   end;
   let i = if is_local_assum decl then i+1 else i in
   (Some kn, i, Projection term::subst)
@@ -594,7 +594,7 @@ let declare_structure ~cumulative finite ~univs ~variances ~primitive_proj
     let cstr = (rsp, 1) in
     let projections = declare_projections rsp (projunivs,ubinders) ~kind inhabitant_id coers implfs fields in
     let build = GlobRef.ConstructRef cstr in
-    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
+    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly ~nonuniform:false in
     let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
     rsp

vernac/vernacentries.ml

@@ -59,17 +59,20 @@ module DefAttributes = struct
     canonical_instance : bool;
     typing_flags : Declarations.typing_flags option;
     using : Vernacexpr.section_subset_expr option;
+    nonuniform : bool
   }
 
-  let parse f =
+  let parse ?(coercion=false) f =
     let open Attributes in
-    let (((((locality, deprecated), polymorphic), program), canonical_instance), typing_flags), using =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using) f
+    let nonuniform = if coercion then ComCoercion.nonuniform else Notations.return None in
+    let ((((((locality, deprecated), polymorphic), program), canonical_instance), typing_flags), using), nonuniform =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using ++ nonuniform) f
     in
     if Option.has_some deprecated then
       Attributes.unsupported_attributes [CAst.make ("deprecated (use a notation and deprecate that instead)",VernacFlagEmpty)];
     let using = Option.map Proof_using.using_from_string using in
-    { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using }
+    let nonuniform = Option.default false nonuniform in
+    { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using; nonuniform }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -87,8 +90,8 @@ let with_module_locality ~atts f =
   let module_local = Attributes.(parse module_locality atts) in
   f ~module_local
 
-let with_def_attributes ~atts f =
-  let atts = DefAttributes.parse atts in
+let with_def_attributes ?coercion ~atts f =
+  let atts = DefAttributes.parse ?coercion atts in
   if atts.DefAttributes.program then Declare.Obls.check_program_libraries ();
   f ~atts
 
@@ -635,9 +638,9 @@ let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook
   (* 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 = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~local ~poly ~nonuniform = let open Decls in function
 | Coercion ->
-  Some (ComCoercion.add_coercion_hook ~poly)
+  Some (ComCoercion.add_coercion_hook ~poly ~nonuniform)
 | CanonicalStructure ->
   Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
@@ -669,7 +672,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 kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~nonuniform:atts.nonuniform kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let typing_flags = atts.typing_flags in
@@ -679,7 +682,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 in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~nonuniform:atts.nonuniform kind in
   let program_mode = atts.program in
   let typing_flags = atts.typing_flags in
   let name = vernac_definition_name lid scope in
@@ -1402,12 +1405,16 @@ let vernac_canonical ~local r =
   Canonical.declare_canonical_structure ?local (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
-  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let (local, poly), nonuniform =
+    Attributes.parse
+      Notations.(locality ++ polymorphic ++ ComCoercion.nonuniform) atts in
   let local = enforce_locality local in
+  let nonuniform = Option.default false nonuniform in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
+  ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~nonuniform
+    ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion ~atts id qids qidt =
@@ -2230,8 +2237,9 @@ let translate_vernac ?loc ~atts v = let open Vernacextend in match v with
   (* Gallina *)
 
   | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) ->
+    let coercion = match discharge with _, Decls.Coercion -> true | _ -> false in
     vtmodifyprogram (fun ~pm ->
-      with_def_attributes ~atts
+      with_def_attributes ~coercion ~atts
        vernac_definition ~pm discharge lid bl red_option c typ)
   | VernacDefinition (discharge,lid,ProveBody(bl,typ)) ->
     vtopenproof(fun () ->