Ensure that names of constants, inductive types or constructors have distinct names and that binders are named

[herbelin]

The PR does the following:

• ensure that Coq objects have distinct names, e.g.:

   Definition f (a a:nat) := a.
   About f.
   (* Before: Arguments f (a a)%nat_scope *)
   (* With the PR: Arguments f (a a0)%nat_scope *)

  Possible alternative: failing instead of renaming silently but this would require adaptations (see note below).

• ensure that binders are named:

  Definition g (_:nat) (P:nat -> Prop) (x : P ltac:(auto)) := x.
  About g.
  (* Before: Arguments g _%nat_scope P%function_scope x *)
  (* With the PR: Arguments g n%nat_scope P%function_scope x *)

  Note: The alternative to force naming user-side would require several changes in the CI.

The last point will be useful for #14597 which requires named binders but for which CI showed that this is sometimes not the case.

See also issue #6786 about non-distinct names in inductive types.

Depends on #18393.

• Added / updated test-suite
• Added changelog.

Note: Here are typical cases which indirectly generate definitions with several times the same name:

• Instantiated definitions

  Definition d1 {y} x (h : x = y :>nat) := h. 
  Definition d2 x := d1 (y:=x).
  About d2.  (* With the PR: "Arguments d2 (x x0)%nat_scope h"; before "(x x)%nat_scope h" *)

• Auxiliary definitions

  Definition idnat (x:nat) := x.
  Definition f (x:nat) := idnat.
  About f. (* With the PR: "Arguments f (x x0)%nat_scope"; before "(x x)%nat_scope" *)

Related issue: avoid the time spent at renaming the types of objects in Typing.type_of_constant & cie.

[ppedrot]

I think that autogenerated names in general are really bad. It's extremely annoying for tactics, but here it's affecting vernacular definitions. The fix goes in the wrong direction for #14597. If one wants to name bound variables, it's the responsibility of the user to name the corresponding definition correctly.

[herbelin]

it's the responsibility of the user to name the corresponding definition correctly.

Yes.

It might be quite a lot of overlays though. We could make an evaluation of the number of changes to do and if too much have a warning as compromise? (Or ask upstreams to do the changes?)

[ppedrot]

I think a warning is a good idea, regardless of the chosen solution.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[ppedrot]

This PR is doing the wrong change. Never ever should we rename binders explicitly given by the user using an freshening algorithm, that would drive people crazy and make the code very much not modular (e.g. when metaprogramming). Similarly, anonymous binders should similarly remain anonymous. Instead, Coq should warn when there are two variables names that conflict and let the user fix the issue, not try to be clever.

[ppedrot]

This is going the wrong way and there is no point in keeping zombie PRs, we should close.

[herbelin]

"zombie PR" is your terminology that I don't endorse! Personally, I would name it an experience which suggests that another approach should be done (in particular in relation to #14597). But that will require some concentration on the topic that I don't have now.