Merge PR #10076: [Canonical structures] Annotation to field declarations to prevent them from being “canonical”

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: robbertkrebbers
Ack-by: vbgl

16 files changed, 145 insertions, 52 deletions

diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+    elpi_CI_REF=canonical-disable-hint
+    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
new file mode 100644
index 0000000000..0a902079b9
--- /dev/null
+++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
@@ -0,0 +1,4 @@
+- Record fields can be annotated to prevent them from being used as canonical projections;
+  see :ref:`canonicalstructures` for details
+  (`#10076 <https://github.com/coq/coq/pull/10076>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index dd21ea09bd..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
@@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we
 are adding to ``EQ`` and ``LE``. In particular it contains the requirement
 that the two relations we are combining are compatible.
 
+The `class_of` projection of the `type` structure is annotated as *not canonical*;
+it plays no role in the search for instances.
+
 Unfortunately there is still an obstacle to developing the algebraic
 theory of this new class.
 
@@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected.
 Unfortunately, these declarations are very verbose. In the following
 subsection we show how to make them more compact.
 
-.. FIXME shouldn't warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Module Add_instance_attempt.
 
@@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-.. FIXME should not warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
   
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 5308330820..ba766c8c3d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
+   .. note::
+      To prevent a field from being involved in the inference of canonical instances,
+      its declaration can be annotated with the :g:`#[canonical(false)]` attribute.
+
+      .. example::
+
+         For instance, when declaring the :g:`Setoid` structure above, the
+         :g:`Prf_equiv` field declaration could be written as follows.
+
+         .. coqdoc::
+
+            #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+
+      See :ref:`canonicalstructures` for a more realistic example.
+
    .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
@@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          Print Canonical Projections.
 
+      .. note::
+
+         The last line would not show up if the corresponding projection (namely
+         :g:`Prf_equiv`) were annotated as not canonical, as described above.
 
 Implicit types of variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e5bf52571c..bb66658a37 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -850,10 +850,10 @@ let rec extern inctx scopes vars r =
 		     | Some c :: q ->
 		         match locs with
 			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-			   | (_, false) :: locs' ->
+                           | { Recordops.pk_true_proj = false } :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
-			   | (_, true) :: locs' ->
+                           | { Recordops.pk_true_proj = true } :: locs' ->
 			       match args with
 				 | [] -> raise No_match
 				     (* we give up since the constructor is not complete *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c0801067ce..f06493b374 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer =
                  let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
-                    | (_, regular) :: proj_kinds ->
+                    | { Recordops.pk_true_proj = regular } :: proj_kinds ->
                        (* "regular" is false when the field is defined
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d69824a256..a23c58c062 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -27,16 +27,27 @@ open Reductionops
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
-(* Table des structures: le nom de la structure (un [inductive]) donne
-   le nom du constructeur, le nombre de paramètres et pour chaque
-   argument réel du constructeur, le nom de la projection
-   correspondante, si valide, et un booléen disant si c'est une vraie
-   projection ou bien une fonction constante (associée à un LetIn) *)
+(* Table of structures.
+   It maps to each structure name (of type [inductive]):
+     - the name of its constructor;
+     - the number of parameters;
+     - for each true argument, some data about the corresponding projection:
+         * its name (may be anonymous);
+         * whether it is a true projection (as opposed to a constant function, LetIn);
+         * whether it should be used as a canonical hint;
+         * the constant realizing this projection (if any).
+*)
+
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
 
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 let structure_table =
@@ -47,7 +58,7 @@ let projection_table =
 (* TODO: could be unify struc_typ and struc_tuple ? *)
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 let register_structure env (id,kl,projs) =
   let open Declarations in
@@ -161,7 +172,7 @@ let canonical_projections () =
     !object_table []
 
 let keep_true_projections projs kinds =
-  let filter (p, (_, b)) = if b then Some p else None in
+  let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in
   List.map_filter filter (List.combine projs kinds)
 
 let rec cs_pattern_of_constr env t =
@@ -206,17 +217,20 @@ let compute_canonical_projections env ~warn (con,ind) =
   let o_NPARAMS = List.length o_TPARAMS in
   let lpj = keep_true_projections lpj kl in
   let nenv = Termops.push_rels_assum sign env in
-  List.fold_left2 (fun acc spopt t ->
-      Option.cata (fun proji_sp ->
-          match cs_pattern_of_constr nenv t with
-          | patt, o_INJ, o_TCOMPS ->
-            ((ConstRef proji_sp, (patt, t)),
-             { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
-            :: acc
-          | exception Not_found ->
-            if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
-            acc
-        ) acc spopt
+  List.fold_left2 (fun acc (spopt, canonical) t ->
+      if canonical
+      then
+        Option.cata (fun proji_sp ->
+            match cs_pattern_of_constr nenv t with
+            | patt, o_INJ, o_TCOMPS ->
+              ((ConstRef proji_sp, (patt, t)),
+               { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+              :: acc
+            | exception Not_found ->
+              if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+              acc
+          ) acc spopt
+      else acc
     ) [] lpj projs
 
 let pr_cs_pattern = function
@@ -288,7 +302,7 @@ let check_and_decompose_canonical_structure env sigma ref =
     with Not_found ->
       error_not_structure ref
         (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
-  let ntrue_projs = List.count snd s.s_PROJKIND in
+  let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f0594d513a..25b6cd0751 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -17,14 +17,20 @@ open Constr
 (** A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
+type proj_kind = {
+  pk_name: Name.t;
+  pk_true_proj: bool;
+  pk_canonical: bool;
+}
+
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (Name.t * bool) list;
+  s_PROJKIND : proj_kind list;
   s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    constructor * (Name.t * bool) list * Constant.t option list
+    constructor * proj_kind list * Constant.t option list
 
 val register_structure : Environ.env -> struc_tuple -> unit
 val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index f4f59a3c16..4717759dec 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -20,6 +20,10 @@ Check ι _ ι.
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
 
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9b8c4efb37..1ad5862d5d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -82,9 +82,12 @@ let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
+let error_twice ~name : 'a =
+  user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
 let assert_once ~name prev =
   if Option.has_some prev then
-    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+    error_twice ~name
 
 let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
   let rec p extra v = function
@@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute =
   attribute_of_list [(on, single_key_parser ~name ~key:on true);
                (off, single_key_parser ~name ~key:off false)]
 
+(* Variant of the [bool] attribute with only two values (bool has three). *)
+let get_bool_value ~key ~default =
+  function
+  | VernacFlagEmpty -> default
+  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
+  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
+
+let enable_attribute ~key ~default : bool attribute =
+  fun atts ->
+  let default = default () in
+  let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in
+  extra,
+  match this with
+  | [] -> default
+  | [ _, value ] -> get_bool_value ~key ~default:true value
+  | _ -> error_twice ~name:key
+
 let qualify_attribute qual (parser:'a attribute) : 'a attribute =
   fun atts ->
     let rec extract extra qualified = function
@@ -139,11 +160,8 @@ let () = let open Goptions in
       optread  = (fun () -> !program_mode);
       optwrite = (fun b -> program_mode:=b) }
 
-let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
-
-let program = program_opt >>= function
-  | Some b -> return b
-  | None -> return (!program_mode)
+let program =
+  enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
@@ -219,3 +237,6 @@ let only_polymorphism atts = parse polymorphic atts
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
 let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+
+let canonical =
+  enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 3cb4d69ca0..44688ddafc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -52,6 +52,7 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
+val canonical : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 94d4ed80d1..6438b48e32 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command"
 
 let subprf = Entry.create "vernac:subprf"
 
+let quoted_attributes = Entry.create "vernac:quoted_attributes"
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
 let def_body = Entry.create "vernac:def_body"
@@ -75,7 +76,7 @@ let parse_compat_version = let open Flags in function
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: vernac_control gallina_ext noedit_mode subprf;
+  GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
   vernac_control: FIRST
     [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
       | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
@@ -447,10 +448,12 @@ GRAMMAR EXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-  [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+  [ [ attr = LIST0 quoted_attributes ;
+      bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
       rf_notation = decl_notation -> {
+      let rf_canonical = attr |> List.flatten |> parse canonical in
       let rf_subclass, rf_decl = bd in
-      rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ]
+      rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;
   record_fields:
     [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
diff --git a/vernac/record.ml b/vernac/record.ml
index f489707eb3..f737a8c524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
   let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
   Termops.substl_rel_context (subst @ subst') fields
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+      (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
         let fi = RelDecl.get_name decl in
         let ti = RelDecl.get_type decl in
 	let (sp_projs,i,subst) =
@@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 	    in
 	    let refi = ConstRef kn in
 	    Impargs.maybe_declare_manual_implicits false refi impls;
-	    if coe then begin
+            if flags.pf_subclass then begin
 	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
 	    end;
 	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
-	      warning_or_error coe indsp why;
+              warning_or_error flags.pf_subclass indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
-      (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+      (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+      (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 open Typeclasses
@@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-      let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
+      let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+                         List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Method ~name:[|binder_name|] record_data
       in
@@ -699,7 +705,11 @@ let definition_structure udecl kind ~template cum poly finite records =
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
-      let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in
+      let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+          { pf_subclass = not (Option.is_empty rf_subclass);
+            pf_canonical = rf_canonical })
+          cfs
+      in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index d6e63901cd..24bb27e107 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,15 +14,20 @@ open Constrexpr
 
 val primitive_flag : bool ref
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 val declare_projections :
   inductive ->
   Entries.universes_entry ->
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
-  bool list ->
+  projection_flags list ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
-    (Name.t * bool) list * Constant.t option list
+    Recordops.proj_kind list * Constant.t option list
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c7795602aa..e1d134f3a9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -744,7 +744,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
-            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a51fdfe59..23633e39ab 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -149,6 +149,7 @@ type record_field_attr = {
   rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
   rf_priority: int option; (* priority of the instance, if relevant *)
   rf_notation: decl_notation list;
+  rf_canonical: bool; (* use this projection in the search for canonical instances *)
   }
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =