Merge PR #13852: [vernac] Improve alpha-renaming in record projection types

Reviewed-by: SkySkimmer

5 files changed, 88 insertions, 5 deletions

diff --git a/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh
new file mode 100644
index 0000000000..9b8d1a63d9
--- /dev/null
+++ b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh
@@ -0,0 +1 @@
+overlay compcert https://github.com/Lysxia/CompCert no-collision-projection 13852
diff --git a/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst
new file mode 100644
index 0000000000..d3ef244cb0
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13852-no-collision-projection.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  In `Record`, alpha-rename the variable associated with the record to avoid
+  alpha-renaming parameters of projections
+  (`#13852 <https://github.com/coq/coq/pull/13852>`_,
+  fixes `#13727 <https://github.com/coq/coq/issues/13727>`_,
+  by Li-yao Xia).
diff --git a/test-suite/output/RecordProjParameter.out b/test-suite/output/RecordProjParameter.out
new file mode 100644
index 0000000000..91ae4b6511
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.out
@@ -0,0 +1,33 @@
+t1 : Atype -> forall a : Type, a
+
+t1 is not universe polymorphic
+Arguments t1 _ _%type_scope
+t1 is transparent
+Expands to: Constant RecordProjParameter.t1
+t3 : forall a0 : Atype, t2 a0
+
+t3 is not universe polymorphic
+t3 is transparent
+Expands to: Constant RecordProjParameter.t3
+u1 : Btype -> forall b b0 : Type, b * b0
+
+u1 is not universe polymorphic
+Arguments u1 _ (_ _)%type_scope
+u1 is transparent
+Expands to: Constant RecordProjParameter.u1
+u3 : forall b1 : Btype, u2 b1
+
+u3 is not universe polymorphic
+u3 is transparent
+Expands to: Constant RecordProjParameter.u3
+v1 : Ctype -> forall c0 : Type, c0
+
+v1 is not universe polymorphic
+Arguments v1 _ _%type_scope
+v1 is transparent
+Expands to: Constant RecordProjParameter.v1
+v3 : forall c : Ctype, v2 c
+
+v3 is not universe polymorphic
+v3 is transparent
+Expands to: Constant RecordProjParameter.v3
diff --git a/test-suite/output/RecordProjParameter.v b/test-suite/output/RecordProjParameter.v
new file mode 100644
index 0000000000..8b892c694c
--- /dev/null
+++ b/test-suite/output/RecordProjParameter.v
@@ -0,0 +1,21 @@
+Record Atype : Type :=
+  { t1 : forall (a : Type), a
+  ; t2 : Type
+  ; t3 : t2 }.
+About t1.
+About t3.
+
+Record Btype : Type :=
+  { u1 : forall (b : Type) (b0 : Type), b * b0
+  ; u2 : Type
+  ; u3 : u2 }.
+About u1.
+About u3.
+
+Record Ctype : Type :=
+  { v1 : forall (c0 : Type), c0
+  ; v2 : Type
+  ; v3 : v2
+  }.
+About v1.
+About v3.
diff --git a/vernac/record.ml b/vernac/record.ml
index 96e4a47d2d..ff6bdc5199 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -511,6 +511,32 @@ let inStruc : Recordops.struc_typ -> Libobject.obj =
 let declare_structure_entry o =
   Lib.add_anonymous_leaf (inStruc o)
 
+(** In the type of every projection, the record is bound to a variable named
+  using the first character of the record type. We rename it to avoid
+  collisions with names already used in the field types.
+*)
+
+(** Get all names bound at the head of [t]. *)
+let rec add_bound_names_constr (names : Id.Set.t) (t : constr) : Id.Set.t =
+  match destProd t with
+  | (b, _, t) ->
+    let names =
+      match b.binder_name with
+      | Name.Anonymous -> names
+      | Name.Name n -> Id.Set.add n names
+    in add_bound_names_constr names t
+  | exception DestKO -> names
+
+(** Get all names bound in any record field. *)
+let bound_names_rdata { DataR.fields; _ } : Id.Set.t =
+  let add_names names field = add_bound_names_constr names (RelDecl.get_type field) in
+  List.fold_left add_names Id.Set.empty fields
+
+(** Pick a variable name for a record, avoiding names bound in its fields. *)
+let data_name { Data.id; Data.rdata; _ } =
+  let name = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in
+  Namegen.next_ident_away name (bound_names_rdata rdata)
+
 (** Main record declaration part:
 
    The entry point is [definition_structure], which will match on the
@@ -537,11 +563,7 @@ let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls par
   in
   let binder_name =
     match name with
-    | None ->
-      let map { Data.id; _ } =
-        Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
-      in
-      Array.map_of_list map record_data
+    | None -> Array.map_of_list data_name record_data
     | Some n -> n
   in
   let ntypes = List.length record_data in