Accept locality attribute for "field" of definitional typeclasses

Should properly fix coq#17451

doc/sphinx/language/core/inductive.rst

@@ -13,7 +13,7 @@ Inductive types
 
    .. prodn::
       inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations }
-      constructor ::= @ident {* @binder } {? @of_type_inst }
+      constructor ::= {* #[ {*, @attribute } ] } @ident {* @binder } {? @of_type_inst }
 
    Defines one or more
    inductive types and its constructors.  Coq generates

doc/tools/docgram/fullGrammar

@@ -932,6 +932,7 @@ decl_notations: [
 
 opt_constructors_or_fields: [
 | ":=" constructors_or_record
+| ":="
 |
 ]
 
@@ -941,11 +942,10 @@ inductive_or_record_definition: [
 
 constructors_or_record: [
 | "|" LIST1 constructor SEP "|"
-| identref constructor_type "|" LIST1 constructor SEP "|"
-| identref constructor_type
-| identref "{" record_fields "}" default_inhabitant_ident
+| LIST0 quoted_attributes identref constructor_type "|" LIST1 constructor SEP "|"
+| LIST0 quoted_attributes identref constructor_type
+| LIST0 quoted_attributes identref "{" record_fields "}" default_inhabitant_ident
 | "{" record_fields "}" default_inhabitant_ident
-|
 ]
 
 default_inhabitant_ident: [
@@ -1021,7 +1021,7 @@ constructor_type: [
 ]
 
 constructor: [
-| identref constructor_type
+| LIST0 quoted_attributes identref constructor_type
 ]
 
 of_type: [

doc/tools/docgram/orderedGrammar

@@ -551,7 +551,7 @@ inductive_definition: [
 ]
 
 constructor: [
-| ident LIST0 binder OPT of_type_inst
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) ident LIST0 binder OPT of_type_inst
 ]
 
 import_categories: [

plugins/funind/glob_term_to_relation.ml

@@ -1480,7 +1480,7 @@ let do_build_inductive evd (funconstants : pconstant list)
   let ext_rels_constructors =
     Array.map
       (List.map (fun (id, t) ->
-           ( Vernacexpr.(NoCoercion, NoInstance)
+           ( Vernacexpr.(Goptions.OptDefault, NoCoercion, NoInstance)
            , ( CAst.make id
              , with_full_print
                  Constrextern.(extern_glob_type empty_extern_env)

test-suite/bugs/bug_17451.v

@@ -0,0 +1,13 @@
+Module Test0.
+
+Class Junk.
+
+Class Dummy : Type :=
+  #[global] something :: Junk.
+
+End Test0.
+
+Section TestSomethingGlobal.
+Variable d : Test0.Dummy.
+Type _ d : Test0.Junk.
+End TestSomethingGlobal.

test-suite/output/bug_16224.out

@@ -1,7 +1,7 @@
 File "./output/bug_16224.v", line 9, characters 0-24:
 Warning: A coercion will be introduced instead of an instance in future
 versions when using ':>' in 'Class' declarations. Replace ':>' with '::' (or
-use '#[global] Existing Instance field.' for compatibility with Coq < 8.17).
+use '#[global] Existing Instance field.' for compatibility with Coq < 8.18).
 Beware that the default locality for '::' is #[export], as opposed to
 #[global] for ':>' currently. Add an explicit #[global] attribute to the
 field if you need to keep the current behavior. For example: "Class foo := {

vernac/comInductive.ml

@@ -721,7 +721,7 @@ let eq_params (up1,p1) (up2,p2) =
 
 let extract_coercions indl =
   let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
-  let iscoe (coe, inst) = match inst with
+  let iscoe (_, coe, inst) = match inst with
     (* remove BackInstanceWarning after deprecation phase *)
     | Vernacexpr.(NoInstance | BackInstanceWarning) -> coe = Vernacexpr.AddCoercion
     | _ -> user_err (Pp.str "'::' not allowed in inductives.") in

vernac/g_vernac.mlg

@@ -87,6 +87,9 @@ let test_id_colon =
     lk_ident >> lk_kw ":"
   end
 
+let parse_attr attr l = parse attr (List.flatten l)
+let unsupported_attr l = unsupported_attributes (List.flatten l)
+
 }
 
 GRAMMAR EXTEND Gram
@@ -393,6 +396,7 @@ GRAMMAR EXTEND Gram
   (* Inductives and records *)
   opt_constructors_or_fields:
     [ [ ":="; lc = constructors_or_record -> { lc }
+      | ":=" -> { Constructors [] }
       | -> { RecordDecl (None, [], None) } ] ]
   ;
   inductive_or_record_definition:
@@ -404,13 +408,16 @@ GRAMMAR EXTEND Gram
   ;
   constructors_or_record:
     [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
-      | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" ->
-          { Constructors ((c id)::l) }
-      | id = identref ; c = constructor_type -> { Constructors [ c id ] }
-      | cstr = identref; "{"; fs = record_fields; "}"; id = default_inhabitant_ident ->
-          { RecordDecl (Some cstr,fs,id) }
-      | "{";fs = record_fields; "}"; id = default_inhabitant_ident -> { RecordDecl (None,fs,id) }
-      |  -> { Constructors [] } ] ]
+      | attr = LIST0 quoted_attributes ; id = identref ; c = constructor_type;
+        "|"; l = LIST1 constructor SEP "|" ->
+          { Constructors ((c attr id)::l) }
+      | attr = LIST0 quoted_attributes ; id = identref ; c = constructor_type ->
+          { Constructors [ c attr id ] }
+      | attr = LIST0 quoted_attributes ;
+        cstr = identref; "{"; fs = record_fields; "}"; id = default_inhabitant_ident ->
+          { let () = unsupported_attr attr in
+            RecordDecl (Some cstr,fs,id) }
+      | "{";fs = record_fields; "}"; id = default_inhabitant_ident -> { RecordDecl (None,fs,id) } ] ]
   ;
   default_inhabitant_ident:
     [ [ "as"; id = identref -> { Some id }
@@ -475,8 +482,8 @@ GRAMMAR EXTEND Gram
   [ [ attr = LIST0 quoted_attributes ;
       bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
       rf_notation = decl_notations -> {
-      let (rf_canonical, rf_reversible), rf_locality = attr |> List.flatten
-        |> parse Notations.(canonical_field ++ reversible ++ option_locality) in
+      let (rf_canonical, rf_reversible), rf_locality =
+        parse_attr Notations.(canonical_field ++ reversible ++ option_locality) attr in
       let (rf_coercion, rf_instance), rf_decl = bd in
       rf_decl,
       { rf_coercion ; rf_reversible ; rf_instance ; rf_priority ; rf_locality ;
@@ -520,15 +527,20 @@ GRAMMAR EXTEND Gram
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_inst; c = lconstr ->
-                    { fun l id -> (coe,(id,mkProdCN ~loc l c)) }
+                    { fun l attr id ->
+                        let locality = parse_attr option_locality attr in
+                        ((locality, fst coe, snd coe),(id,mkProdCN ~loc l c)) }
             |  ->
-                 { fun l id -> ((NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous)))) } ]
+                 { fun l attr id ->
+                     let () = unsupported_attr attr in
+                     ((Goptions.OptDefault,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous)))) } ]
          -> { t l }
      ]]
 ;
 
   constructor:
-    [ [ id = identref; c=constructor_type -> { c id } ] ]
+    [ [ attr = LIST0 quoted_attributes ;
+        id = identref; c=constructor_type -> { c attr id } ] ]
   ;
   of_type:
     [ [   ":>" -> { AddCoercion }

vernac/ppvernac.ml

@@ -845,7 +845,7 @@ let pr_synpure_vernac_expr v =
     return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
                    pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
   | VernacInductive (f,l) ->
-    let pr_constructor ((coe,ins),(id,c)) =
+    let pr_constructor ((_,coe,ins),(id,c)) =
       hov 2 (pr_lident id ++ pr_oc coe ins ++
              Flags.without_option Flags.beautify pr_spc_lconstr c)
     in

vernac/record.ml

@@ -644,8 +644,9 @@ let warn_future_coercion_class_field =
   CWarnings.create ~name:"future-coercion-class-field" ~category:Deprecation.Version.v8_17
     Pp.(fun definitional ->
     strbrk "A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. "
-    ++ strbrk "Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.17). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently."
-    ++ strbrk (if definitional then "" else " Add an explicit #[global] attribute to the field if you need to keep the current behavior. For example: \"Class foo := { #[global] field :: bar }.\""))
+    ++ strbrk "Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.18). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently."
+    ++ strbrk (if definitional then " Add an explicit #[global] attribute if you need to keep the current behavior. For example: \"Class foo := #[global] baz :: bar.\""
+               else " Add an explicit #[global] attribute to the field if you need to keep the current behavior. For example: \"Class foo := { #[global] field :: bar }.\""))
 
 let check_proj_flags kind rf =
   let open Vernacexpr in

vernac/vernacentries.ml

@@ -929,10 +929,10 @@ let preprocess_inductive_decl ~atts kind indl =
     in
     if fst id = AddCoercion then
       user_err Pp.(str "Definitional classes do not support the \">\" syntax.");
-    let ((rf_coercion, rf_instance), (lid, ce)) = l in
+    let ((rf_locality, rf_coercion, rf_instance), (lid, ce)) = l in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
             { rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
-              rf_locality = Goptions.OptDefault ; rf_notation = [] ; rf_canonical = true } in
+              rf_locality ; rf_notation = [] ; rf_canonical = true } in
     let recordl = [id, bl, c, None, [f], None] in
     let kind = Class true in
     let records = vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags ~primitive_proj finite recordl in

vernac/vernacexpr.mli

@@ -190,7 +190,7 @@ type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
-type 'a with_coercion_instance = (coercion_flag * instance_flag) * 'a
+type 'a with_coercion_instance = (Goptions.option_locality * coercion_flag * instance_flag) * 'a
 (* Attributes of a record field declaration *)
 type record_field_attr = {
   rf_coercion: coercion_flag; (* the projection is an implicit coercion *)