Merge PR #11164: [CS] allow Let variable to be canonical

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot

11 files changed, 98 insertions, 38 deletions

diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst
new file mode 100644
index 0000000000..b9ecd140e7
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst
@@ -0,0 +1 @@
+- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index e746096df2..bdfdffeaad 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1983,6 +1983,8 @@ Deactivation of implicit arguments for parsing
    to be given as if no arguments were implicit. By symmetry, this also
    affects printing.
 
+.. _canonical-structure-declaration:
+
 Canonical structures
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -1993,6 +1995,7 @@ value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
 .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
+  :name: Canonical Structure
 
    This command declares :token:`qualid` as a canonical instance of a
    structure (a record). When the :g:`#[local]` attribute is given the effect
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 70dadedd35..d591718b17 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1620,6 +1620,17 @@ variety of commands:
        :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
        :n:`@string__3` is the note.
 
+``canonical``
+    This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
+    It is equivalent to having a :cmd:`Canonical Structure` declaration just
+    after the command.
+
+    This attirbute can take the value ``false`` when decorating a record field
+    declaration with the effect of preventing the field from being involved in
+    the inference of canonical instances.
+
+    See also :ref:`canonical-structure-declaration`.
+
 .. example::
 
    .. coqtop:: all reset warn
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 35e182840b..4046419bd5 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open CErrors
 open Util
 open Pp
 open Names
-open Globnames
 open Constr
 open Mod_subst
 open Reductionops
@@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) =
      (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = subst_constructor subst id in
+  let id' = Globnames.subst_constructor subst id in
   if projs' == projs && id' == id then obj else
     (id',kl,projs')
 
@@ -190,13 +189,13 @@ let rec cs_pattern_of_constr env t =
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
-  | _ -> Const_cs (global_of_constr t) , None, []
+  | _ -> Const_cs (Globnames.global_of_constr t) , None, []
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (sign,env,t,con,proji_sp) ->
+         (fun (sign,env,t,ref,proji_sp) ->
           let env = Termops.push_rels_assum sign env in
-          let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in
+          let con_pp = Nametab.pr_global_env Id.Set.empty ref in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in
           let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
@@ -204,11 +203,16 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections env ~warn (con,ind) =
-  let o_CTX = Environ.constant_context env con in
-  let u = Univ.make_abstract_instance o_CTX in
-  let o_DEF = mkConstU (con, u) in
-  let c = Environ.constant_value_in env (con,u) in
+let compute_canonical_projections env ~warn (gref,ind) =
+  let o_CTX = Environ.universes_of_global env gref in
+  let o_DEF, c =
+    match gref with
+    | GlobRef.ConstRef con ->
+        let u = Univ.make_abstract_instance o_CTX in
+        mkConstU (con, u), Environ.constant_value_in env (con,u)
+    | GlobRef.VarRef id ->
+        mkVar id, Option.get (Environ.named_body id env)
+    | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false in
   let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
@@ -230,7 +234,7 @@ let compute_canonical_projections env ~warn (con,ind) =
                { o_ORIGIN = con ; 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);
+              if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
               acc
           ) acc spopt
       else acc
@@ -266,12 +270,17 @@ let register_canonical_structure ~warn env sigma o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
-let subst_canonical_structure subst (cst,ind as obj) =
+type cs = GlobRef.t * inductive
+
+let subst_canonical_structure subst (gref,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
-  let cst' = subst_constant subst cst in
-  let ind' = subst_ind subst ind in
-  if cst' == cst && ind' == ind then obj else (cst',ind')
+  match gref with
+  | GlobRef.ConstRef cst ->
+      let cst' = subst_constant subst cst in
+      let ind' = subst_ind subst ind in
+      if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind')
+  | _ -> assert false
 
 (*s High-level declaration of a canonical structure *)
 
@@ -282,15 +291,20 @@ let error_not_structure ref description =
           description))
 
 let check_and_decompose_canonical_structure env sigma ref =
-  let sp =
+  let vc =
     match ref with
-      GlobRef.ConstRef sp -> sp
-    |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
+    | GlobRef.ConstRef sp ->
+        let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
+        begin match Environ.constant_opt_value_in env (sp, u) with
+        | Some vc -> vc
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.VarRef id ->
+        begin match Environ.named_body id env with
+        | Some b -> b
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.IndRef _ | GlobRef.ConstructRef _ ->
+        error_not_structure ref (str "Expected an instance of a record or structure.")
   in
-  let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
-  let vc = match Environ.constant_opt_value_in env (sp, u) with
-    | Some vc -> vc
-    | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
   let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
@@ -308,7 +322,7 @@ let check_and_decompose_canonical_structure env sigma ref =
   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)
+  (ref,indsp)
 
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (GlobRef.Map.find proj !object_table)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index aaba7cc3e5..7eac0ddf52 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -87,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 
 val pr_cs_pattern : cs_pattern -> Pp.t
 
+type cs = GlobRef.t * inductive
+
 val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
 val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
-  Constant.t * inductive -> unit
-val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive
+  cs -> unit
+val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
 
-val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive
+val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index e6d674c1e6..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2).
 Check s0.
 Check s1.
 Check s2.
+
+Section Y.
+  Let s3 := MKL x3.
+  Canonical Structure s3.
+  Check (refl_equal _ : l _ = x3).
+End Y.
+Fail Check (refl_equal _ : l _ = x3).
+Fail Check s3.
+
+Section V.
+  #[canonical] Let s3 := MKL x3.
+  Check (refl_equal _ : l _ = x3).
+End V.
+
+Section W.
+  #[canonical, local] Definition s2' := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+End W.
+Fail Check (refl_equal _ : l _ = x2).
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index b7a3b002bd..68d2c3a00d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -234,5 +234,7 @@ 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 =
+let canonical_field =
   enable_attribute ~key:"canonical" ~default:(fun () -> true)
+let canonical_instance =
+  enable_attribute ~key:"canonical" ~default:(fun () -> false)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 34ff15ca7d..0074db66d3 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -48,7 +48,8 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : Deprecation.t option attribute
-val canonical : bool attribute
+val canonical_field : bool attribute
+val canonical_instance : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 141b02ef63..e41610b532 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) =
   let sigma = Evd.from_env env in
   register_canonical_structure ~warn:true env sigma o
 
-let discharge_canonical_structure (_,(x, local)) =
-  if local then None else Some (x, local)
+let discharge_canonical_structure (_,((gref, _ as x), local)) =
+  if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
+  else Some (x, local)
 
-let inCanonStruc : (Constant.t * inductive) * bool -> obj =
+
+let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
                   open_function = open_canonical_structure;
                   cache_function = cache_canonical_structure;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 69ab0fafe9..3302231fd1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram
   [ [ 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_canonical = attr |> List.flatten |> parse canonical_field in
       let rf_subclass, rf_decl = bd in
       rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 99d74f16cc..e98820bc98 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -63,14 +63,15 @@ module DefAttributes = struct
     polymorphic : bool;
     program : bool;
     deprecated : Deprecation.t option;
+    canonical_instance : bool;
   }
 
   let parse f =
     let open Attributes in
-    let ((locality, deprecated), polymorphic), program =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+    let (((locality, deprecated), polymorphic), program), canonical_instance =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
     in
-    { polymorphic; program; locality; deprecated }
+    { polymorphic; program; locality; deprecated; canonical_instance }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   in
   start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
-let vernac_definition_hook ~local ~poly = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
   Some (ComCoercion.add_coercion_hook ~poly)
 | CanonicalStructure ->
   Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
   Some (ComCoercion.add_subclass_hook ~poly)
+| Definition when canonical_instance ->
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+| Let when canonical_instance ->
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
 | _ -> None
 
 let fresh_name_for_anonymous_theorem () =
@@ -551,7 +556,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 ~local:atts.locality ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
@@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
 let vernac_definition ~atts (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 ~local:atts.locality ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let name = vernac_definition_name lid scope in
   let red_option = match red_option with