Merge PR #14041: Enable canonical fun _ => _ projections.

Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer

8 files changed, 104 insertions, 10 deletions

diff --git a/doc/changelog/12-misc/14041-cs_lambda.rst b/doc/changelog/12-misc/14041-cs_lambda.rst
new file mode 100644
index 0000000000..872b1f09eb
--- /dev/null
+++ b/doc/changelog/12-misc/14041-cs_lambda.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Enable canonical `fun _ => _` projections,
+  see :ref:`canonicalstructures` for details.
+  (`#14041 <https://github.com/coq/coq/pull/14041>`_,
+  by Jan-Oliver Kaiser and Pierre Roux,
+  reviewed by Cyril Cohen and Enrico Tassi).
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index fbba6c30b8..e3b014d8d5 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -41,12 +41,54 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    This command supports the :attr:`local` attribute.  When used, the
    structure is canonical only within the :cmd:`Section` containing it.
 
-   Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
-   structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
-   Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+   :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the
+   structure :g:`struct` for which the fields are :n:`x__1, …, x__n`.
+   Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be
    solved during the type checking process, :token:`qualid` is used as a solution.
-   Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
-   into a complete structure built on |c_i|.
+   Otherwise said, :token:`qualid` is canonically used to extend the field :n:`x__i`
+   into a complete structure built on :n:`c__i` when :n:`c__i` unifies with :n:`(x__i _)`.
+
+   The following kinds of terms are supported for the fields :n:`c__i` of :token:`qualid`:
+
+   * :term:`Constants <constant>` and section variables of an active section,
+     applied to zero or more arguments.
+   * :token:`sort`\s.
+   * Literal functions:  `fun … => …`.
+   * Literal, non-dependent function types, i.e. implications: `… -> …`.
+   * Variables bound in :token:`qualid`.
+
+   Only the head symbol of an existing instance's field :n:`c__i`
+   is considered when searching for a canonical extension.
+   We call this head symbol the *key* and we say ":token:`qualid` *keys* the field :n:`x__i` to :n:`k`" when :n:`c__i`'s
+   head symbol is :n:`k`.
+   Keys are the only piece of information that is used for canonical extension.
+   The keys corresponding to the kinds of terms listed above are:
+
+   * For constants and section variables, potentially applied to arguments:
+     the constant or variable itself, disregarding any arguments.
+   * For sorts: the sort itself.
+   * For literal functions: skip the abstractions and use the key of the body.
+   * For literal functions types: a disembodied implication key denoted `_ -> _`, disregarding both its
+     domain and codomain.
+   * For variables bound in :token:`qualid`: a catch-all key denoted `_`.
+
+   This means that, for example, `(some_constant x1)` and `(some_constant (other_constant y1 y2) x2)`
+   are not distinct keys.
+
+   Variables bound in :token:`qualid` match any term for the purpose of canonical extension.
+   This has two major consequences for a field :n:`c__i` keyed to a variable of :token:`qualid`:
+
+   1. Unless another key—and, thus, instance—matches :n:`c__i`, the instance will always be considered by
+      unification.
+   2. :n:`c__i` will be considered overlapping not distinct from any other canonical instance
+      that keys :n:`x__i` to one of its own variables.
+
+   A record field :n:`x__i` can only be keyed once to each key.
+   Coq prints a warning when :token:`qualid` keys :n:`x__i` to a term
+   whose head symbol is already keyed by an existing canonical instance.
+   In this case, Coq will not register that :token:`qualid` as a canonical
+   extension.
+   (The remaining fields of the instance can still be used for canonical extension.)
 
    Canonical structures are particularly useful when mixed with coercions
    and strict implicit arguments.
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5eb8a88698..d6ba84d0bf 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -232,7 +232,17 @@ let occur_rigidly flags env evd (evk,_) t =
 let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let open ValuePattern in
   let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
+  let t2, sk2' = decompose_app_vect sigma (shrink_eta env t2) in
+  let sk2 = Stack.append_app sk2' sk2 in
   let (sigma, solution), sk2_effective =
+    let t2 =
+      let rec remove_lambda t2 =
+        match EConstr.kind sigma t2 with
+        | Lambda (_,_,t2) -> remove_lambda t2
+        | Cast (t2,_,_) -> remove_lambda t2
+        | App (t2,_) -> t2
+        | _ -> t2 in
+      if Stack.is_empty sk2 then remove_lambda t2 else t2 in
     try
       match EConstr.kind sigma t2 with
         Prod (_,a,b) -> (* assert (l2=[]); *)
diff --git a/pretyping/structures.ml b/pretyping/structures.ml
index 3ef6e98373..145663d3b9 100644
--- a/pretyping/structures.ml
+++ b/pretyping/structures.ml
@@ -161,6 +161,7 @@ let rec of_constr env t =
     let patt, n, args = of_constr env f in
     patt, n, args @ Array.to_list vargs
   | Rel n -> Default_cs, Some n, []
+  | Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
   | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
@@ -222,6 +223,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
   let lpj = keep_true_projections lpj in
   let nenv = Termops.push_rels_assum sign env in
   List.fold_left2 (fun acc (spopt, canonical) t ->
+      let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in
       if canonical
       then
         Option.cata (fun proji_sp ->
diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
index a70f8ca45a..23119bab97 100644
--- a/test-suite/output/Warnings.out
+++ b/test-suite/output/Warnings.out
@@ -1,3 +1,4 @@
 File "stdin", line 4, characters 0-22:
-Warning: Projection value has no head constant: fun x : B => x in canonical
-instance a of b, ignoring it. [projection-no-head-constant,typechecker]
+Warning: Projection value has no head constant: forall x : nat, x > 0 in
+canonical instance a of b, ignoring it.
+[projection-no-head-constant,typechecker]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 7465442cab..ce92bcbbb2 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-Record A := { B:Type; b:B->B }.
-Definition a B := {| B:=B; b:=fun x => x |}.
+Record A := { B:Type; b:Prop }.
+Definition a B := {| B:=B; b:=forall x, x > 0 |}.
 Canonical Structure a.
 
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 88702a6e80..a833dd0bd6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -70,3 +70,35 @@ Section W.
   Check (refl_equal _ : l _ = x2).
 End W.
 Fail Check (refl_equal _ : l _ = x2).
+
+(* Lambda keys *)
+Section L1.
+  Structure cs_lambda := { cs_lambda_key : nat -> nat }.
+  #[local] Canonical Structure cs_lambda_func :=
+    {| cs_lambda_key := fun x => x + 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _).
+End L1.
+
+Section L2.
+  #[local] Canonical Structure cs_lambda_func2 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L2.
+
+Section L3.
+  #[local] Canonical Structure cs_lambda_func3 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L3.
+
+Section L4.
+  #[local] Canonical Structure cs_lambda_func4 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L4.
+
+Section L5.
+  #[local] Canonical Structure cs_lambda_func5 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L5.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index d8eb005ab2..72e6e757d3 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -297,7 +297,6 @@ Require Import ssreflect ssrfun.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-Set Warnings "-projection-no-head-constant".
 
 Notation reflect := Bool.reflect.
 Notation ReflectT := Bool.ReflectT.
@@ -1227,7 +1226,9 @@ Definition clone_pred T U :=
 Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope.
 
 Canonical predPredType T := PredType (@id (pred T)).
+Set Warnings "-redundant-canonical-projection".
 Canonical boolfunPredType T := PredType (@id (T -> bool)).
+Set Warnings "redundant-canonical-projection".
 
 (** The type of abstract collective predicates.
  While {pred T} is contertible to pred T, it presents the pred_sort coercion