Uniformize semantics of :> in class after deprecation phase of rocq-prover#16230

This ends the deprecation phases of
rocq-prover#16230 and
rocq-prover#15802
that introduced :: instead of :> for subclasses in Class declarations.
Now :> means coercion in all record declarations (including typeclasses).

Author: proux01

doc/sphinx/addendum/type-classes.rst

@@ -309,9 +309,8 @@ Command summary
    declared rigid during resolution so that the typeclass abstraction is
    maintained.
 
-   The `>` in
-   :token:`record_definition` currently does nothing. In a future version, it will
-   create coercions as it does when used in :cmd:`Record` commands.
+   The `>` in :token:`record_definition`
+   creates coercions as it does when used in :cmd:`Record` commands.
 
    Like any command declaring a record, this command supports the
    :attr:`universes(polymorphic)`, :attr:`universes(template)`,
@@ -342,18 +341,9 @@ Command summary
 
          This command has no effect when used on a typeclass.
 
-.. _warn-future-coercion-class-field:
-
-   .. warn:: 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).
-
-      In future versions, :g:`:>` in the :n:`@record_definition` or
-      :n:`@constructor` will declare a :ref:`coercion<coercions>`, as
-      it does for other :cmd:`Record` commands. To eliminate the warning, use
-      :g:`::` instead.
-
    .. warn:: Ignored instance declaration for “@ident”: “@term” is not a class
 
-      Using the ``::`` (or deprecated ``:>``) syntax in the :n:`@record_definition`
+      Using the ``::`` syntax in the :n:`@record_definition`
       or :n:`@constructor` with a right-hand-side that
       is not itself a Class has no effect (apart from emitting this warning).
 

doc/sphinx/language/core/records.rst

@@ -92,7 +92,6 @@ Defining record types
      :n:`:>`
        If specified, the field is declared as a coercion from the record name
        to the class of the field type. See :ref:`coercions`.
-       Note that this currently does something else in :cmd:`Class` commands.
 
      :n:`::`
        If specified, the field is declared a typeclass instance of the class

test-suite/output/bug_16224.out

@@ -1,4 +1,5 @@
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
+[cic] : Cic >-> A (reversible)
 [rc] : Rc >-> A (reversible)
 [ric] : Ric >-> A (reversible)
 ric : Ric -> A

test-suite/success/record_field_coercion_tc.v

@@ -0,0 +1,75 @@
+Module RecordNothing.
+Class B.
+Record A := { ab : B }.
+Parameter a : A.
+Fail Check a : B.  (* no coercion *)
+Existing Class A.
+Existing Instance a.
+Fail Type _ : B.  (* no typeclass instance *)
+End RecordNothing.
+
+Module RecordCoercion.
+Class B.
+Record A := { ab :> B }.
+Parameter a : A.
+Check a : B.  (* coercion *)
+Existing Class A.
+Existing Instance a.
+Fail Type _ : B.  (* no typeclass instance *)
+End RecordCoercion.
+
+Module RecordTC.
+Class B.
+Record A := { ab :: B }.
+Parameter a : A.
+Fail Check a : B.  (* no coercion *)
+Existing Class A.
+Existing Instance a.
+Type _ : B.  (* typeclass instance *)
+End RecordTC.
+
+Module RecordCoercionTC.
+Class B.
+Record A := { ab ::> B }.
+Parameter a : A.
+Check a : B.  (* coercion *)
+Existing Class A.
+Existing Instance a.
+Type _ : B.  (* typeclass instance *)
+End RecordCoercionTC.
+
+Module ClassNothing.
+Class B.
+Class A := { ab : B }.
+Parameter a : A.
+Fail Check a : B.  (* no coercion *)
+Existing Instance a.
+Fail Type _ : B.  (* no typeclass instance *)
+End ClassNothing.
+
+Module ClassCoercion.
+Class B.
+Class A := { ab :> B }.
+Parameter a : A.
+Check a : B.  (* coercion *)
+Existing Instance a.
+Fail Type _ : B.  (* no typeclass instance *)
+End ClassCoercion.
+
+Module ClassTC.
+Class B.
+Class A := { ab :: B }.
+Parameter a : A.
+Fail Check a : B.  (* no coercion *)
+Existing Instance a.
+Type _ : B.  (* typeclass instance *)
+End ClassTC.
+
+Module ClassCoercionTC.
+Class B.
+Class A := { ab ::> B }.
+Parameter a : A.
+Check a : B.  (* coercion *)
+Existing Instance a.
+Type _ : B.  (* typeclass instance *)
+End ClassCoercionTC.

vernac/comInductive.ml

@@ -735,8 +735,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
-    (* remove BackInstanceWarning after deprecation phase *)
-    | Vernacexpr.(NoInstance | BackInstanceWarning) -> coe = Vernacexpr.AddCoercion
+    | Vernacexpr.NoInstance -> coe = Vernacexpr.AddCoercion
     | _ -> user_err (Pp.str "'::' not allowed in inductives.") in
   let extract lc = List.filter (fun (coe,_) -> iscoe coe) lc in
   List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))

vernac/g_vernac.mlg

@@ -615,8 +615,8 @@ GRAMMAR EXTEND Gram
         | ":" -> { NoCoercion } ] ]
   ;
   of_type_inst:
-    [ [   ":>" -> { (AddCoercion, BackInstanceWarning) (* replace with NoInstance at end of deprecation phase *) }
-        | ":"; ">" -> { (AddCoercion, BackInstanceWarning) (* replace with NoInstance at end of deprecation phase *) }
+    [ [   ":>" -> { (AddCoercion, NoInstance) }
+        | ":"; ">" -> { (AddCoercion, NoInstance) }
         | "::" -> { (NoCoercion, BackInstance) }
         | "::>" -> { (AddCoercion, BackInstance) }
         | ":" -> { (NoCoercion, NoInstance) } ] ]

vernac/ppvernac.ml

@@ -566,7 +566,6 @@ let pr_oc coe ins = match coe, ins with
   | AddCoercion, NoInstance -> str" :>"
   | NoCoercion, BackInstance -> str" ::"
   | AddCoercion, BackInstance -> str" ::>"
-  | _, BackInstanceWarning -> str" :>"  (* remove this line at end of deprecation phase *)
 
 let pr_record_field (x, { rfu_attrs = attr ; rfu_coercion = coe ; rfu_instance = ins ; rfu_priority = pri ; rfu_notation = ntn }) =
   let prx = match x with

vernac/record.ml

@@ -391,10 +391,8 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
 
 (** Declare projection [ref] over [from] a coercion
    or a typeclass instance according to [flags]. *)
-(* remove the last argument (it will become alway true) after deprecation phase
-   (started in 8.17, c.f. https://github.com/coq/coq/pull/16230) *)
-let declare_proj_coercion_instance ~flags ref from ~with_coercion =
-  if with_coercion && flags.Data.pf_coercion then begin
+let declare_proj_coercion_instance ~flags ref from =
+  if 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 ~reversible:flags.Data.pf_reversible ~source:cl
@@ -466,7 +464,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
   in
   let refi = GlobRef.ConstRef kn in
   Impargs.maybe_declare_manual_implicits false refi impls;
-  declare_proj_coercion_instance ~flags refi (GlobRef.IndRef indsp) ~with_coercion:true;
+  declare_proj_coercion_instance ~flags refi (GlobRef.IndRef indsp);
   let i = if is_local_assum decl then i+1 else i in
   (Some kn, i, Projection term::subst)
 
@@ -683,38 +681,18 @@ let implicits_of_context ctx =
          | LocalAssum _ as d -> Some (RelDecl.get_name d))
          ctx)))
 
-(* deprecated in 8.16, to be removed at the end of the deprecation phase
-   (c.f., https://github.com/coq/coq/pull/15802 ) *)
-let warn_future_coercion_class_constructor =
-  CWarnings.create ~name:"future-coercion-class-constructor" ~category:Deprecation.Version.v8_16
-    ~default:CWarnings.AsError
-    Pp.(fun () -> str "'Class >' currently does nothing. Use 'Class' instead.")
-
-(* deprecated in 8.17, to be removed at the end of the deprecation phase
-   (c.f., https://github.com/coq/coq/pull/16230 ) *)
-let warn_future_coercion_class_field =
-  CWarnings.create ~name:"future-coercion-class-field" ~category:Deprecation.Version.v8_17
-    ~default:CWarnings.AsError
-    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.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
   let pf_coercion, pf_reversible =
     match rf.rf_coercion with
-    (* replace "kind_class kind = NotClass" with true after deprecation phase *)
-    | AddCoercion -> kind_class kind = NotClass, Option.default true rf.rf_reversible
+    | AddCoercion -> true, Option.default true rf.rf_reversible
     | NoCoercion ->
        if rf.rf_reversible <> None then
          Attributes.(unsupported_attributes
            [CAst.make ("reversible (without :>)",VernacFlagEmpty)]);
        false, false in
   let pf_instance =
-    match rf.rf_instance with NoInstance -> false | BackInstance -> true
-    | BackInstanceWarning -> kind_class kind <> NotClass in
+    match rf.rf_instance with NoInstance -> false | BackInstance -> true in
   let pf_priority = rf.rf_priority in
   let pf_locality =
     begin match rf.rf_coercion, rf.rf_instance with
@@ -728,19 +706,10 @@ let check_proj_flags kind rf =
            [CAst.make ("export (without ::)",VernacFlagEmpty)])
     | _ -> ()
     end; rf.rf_locality in
-  (* remove following let after deprecation phase (started in 8.17,
-     c.f., https://github.com/coq/coq/pull/16230 ) *)
-  let pf_locality =
-    match rf.rf_instance, rf.rf_locality with
-    | BackInstanceWarning, Goptions.OptDefault -> Goptions.OptGlobal
-    | _ -> pf_locality in
   let pf_canonical = rf.rf_canonical in
   Data.{ pf_coercion; pf_reversible; pf_instance; pf_priority; pf_locality; pf_canonical }
 
-(* remove the definitional argument at the end of the deprecation phase
-   (started in 8.17)
-   (c.f., https://github.com/coq/coq/pull/16230 ) *)
-let pre_process_structure ?(definitional=false) ~auto_prop_lowering udecl kind ~poly (records : Ast.t list) =
+let pre_process_structure ~auto_prop_lowering udecl kind ~poly (records : Ast.t list) =
   let indlocs = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
@@ -767,11 +736,6 @@ let pre_process_structure ?(definitional=false) ~auto_prop_lowering udecl kind ~
         Namegen.next_ident_away canonical_inhabitant_id (bound_names_rdata rdata)
     in
     let is_coercion = match is_coercion with AddCoercion -> true | NoCoercion -> false in
-    if kind_class kind <> NotClass then begin
-      if is_coercion then warn_future_coercion_class_constructor ();
-      if List.exists (function (_, Vernacexpr.{ rf_instance = BackInstanceWarning; _ }) -> true | _ -> false) cfs then
-        warn_future_coercion_class_field definitional
-    end;
     { Data.id = name.CAst.v; idbuild; rdata; is_coercion; proj_flags; inhabitant_id }
   in
   let data = List.map2 map data records in
@@ -920,7 +884,7 @@ let declare_class_constant ~univs paramimpls params data =
   Classes.set_typeclass_transparency ~locality:Hints.SuperGlobal
     [Evaluable.EvalConstRef cst] false;
   let () =
-    declare_proj_coercion_instance ~flags:proj_flags (GlobRef.ConstRef proj_cst) cref ~with_coercion:false in
+    declare_proj_coercion_instance ~flags:proj_flags (GlobRef.ConstRef proj_cst) cref in
   let m = {
     meth_name = Name proj_name;
     meth_info = None;
@@ -1086,16 +1050,11 @@ let definition_structure ~flags udecl kind ~primitive_proj (records : Ast.t list
       finite;
     } = flags in
   let impargs, params, univs, variances, projections_kind, data, indlocs =
-    let definitional = kind_class kind = DefClass in
-    pre_process_structure ~auto_prop_lowering ~definitional udecl kind ~poly records
+    pre_process_structure ~auto_prop_lowering udecl kind ~poly records
   in
   let inds, def = match kind_class kind with
     | DefClass -> declare_class_constant ~univs impargs params data
     | RecordClass | NotClass ->
-      (* remove the following block after deprecation phase
-         (started in 8.16, c.f., https://github.com/coq/coq/pull/15802 ) *)
-      let data = if kind_class kind = NotClass then data else
-          List.map (fun d -> { d with Data.is_coercion = false }) data in
       let structure =
         interp_structure_core
           ~cumulative finite ~univs ~variances ~primitive_proj

vernac/vernacentries.ml

@@ -918,7 +918,7 @@ let preprocess_inductive_decl ~atts kind indl =
       user_err Pp.(str "Definitional classes do not support the \">\" syntax.");
     let ((attr, rf_coercion, rf_instance), (lid, ce)) = l in
     let rf_locality = match rf_coercion, rf_instance with
-      | AddCoercion, _ | _, (BackInstance | BackInstanceWarning) -> parse option_locality attr
+      | AddCoercion, _ | _, BackInstance -> parse option_locality attr
       | _ -> let () = unsupported_attributes attr in Goptions.OptDefault in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
             { rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
@@ -946,7 +946,7 @@ let preprocess_inductive_decl ~atts kind indl =
           | AddCoercion -> reversible
           | NoCoercion -> Notations.return None in
         let loc = match f.rfu_coercion, f.rfu_instance with
-          | AddCoercion, _ | _, (BackInstance | BackInstanceWarning) -> option_locality
+          | AddCoercion, _ | _, BackInstance -> option_locality
           | _ -> Notations.return Goptions.OptDefault in
         Notations.(rev ++ loc ++ canonical_field) in
       let (rf_reversible, rf_locality), rf_canonical = parse attr f.rfu_attrs in

vernac/vernacexpr.mli

@@ -110,10 +110,7 @@ type 'a search_restriction =
 
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = AddCoercion | NoCoercion
-(* Remove BackInstanceWarning at end of deprecation phase
-   (this is just to print a warning when :> is used instead of ::
-   to declare instances in classes) *)
-type instance_flag  = BackInstance | BackInstanceWarning | NoInstance
+type instance_flag  = BackInstance | NoInstance
 
 type export_flag = Lib.export_flag = Export | Import