Equations generates wrong variable names

[fkj]

In some cases, when trying to prove termination by a well-foundedness argument, the generated proof obligations are unprovable due to overlapping variable names which are not correctly handled.
The issue occurs when defining a function over an inductive definition where the function pattern matches using the same variable names as the names in the inductive definition.
I guess the issue is that the names in the inductive definition are used as default names in the proof obligations and that Equations somehow fails to prevent these names from overlapping with other names in the equation, and thus renames only some of the variables to something else.
It does not seem that there is any risk of unsoundness from this issue since the goals simply become unprovable in all of the cases of this I have encountered so far.

The issue can be worked around either by renaming some of the variables (in the inductive definition or in the pattern matching), or by introducing an extra case in the pattern match which explicitly names the variables in the involved cases.

I am using Coq 8.15.0 and Equations 1.3+8.15.

Here is an example (I am not allowed to attach it as a file for some reason) which shows the issue and the workarounds mentioned above:

From Equations Require Import Equations.
Require Import List.
Import ListNotations.
Require Import Lia.

Inductive tree : Type :=
| Leaf (n : nat)
| Node (p : tree) (q : tree).

Fixpoint tree_size (t : tree) : nat :=
  match t with
  | Leaf _ => 1
  | Node a b => 1 + tree_size a + tree_size b
  end.

Fixpoint trees_size (ts : list tree) : nat :=
  match ts with
  | [] => 0
  | x :: xs => tree_size x + trees_size xs
  end.

Equations? silly (a b : list nat) (c d : list tree) : bool by wf (trees_size c + trees_size d) lt :=
  silly a b (Node p q :: c) [] => false;
  silly a b c (Node p q :: d) => silly a b (p :: c) (q :: d);
  silly a b c d => false.
Proof.
  - lia.
  - lia.
  - Fail lia. (* some variables are called p0 and q0 when they should be p and q! *)
Abort.

(* It works if we add an extra case with explicit names: *)
Equations? silly2 (a b : list nat) (c d : list tree) : bool by wf (trees_size c + trees_size d) lt :=
  silly2 a b (Node p q :: c) [] => false;
  (* we add an extra case naming the variable explicitly to avoid overlap *)
  silly2 a b (Node r s :: c) (Node p q :: d) => silly2 a b (p :: Node r s :: c) (q :: d);
  silly2 a b c (Node p q :: d) => silly2 a b (p :: c) (q :: d);
  silly2 a b c d => false.
Proof.
  - lia.
  - lia.
  - lia. (* now names are chosen correctly! *)
Qed.

(* It also works if the names don't overlap: *)
Equations? silly3 (a b : list nat) (c d : list tree) : bool by wf (trees_size c + trees_size d) lt :=
  silly3 a b (Node p q :: c) [] => false;
  silly3 a b c (Node x y :: d) => silly3 a b (x :: c) (y :: d);
  silly3 a b c d => false.
Proof.
  - lia.
  - lia.
  - lia. (* now names are chosen correctly! *)
Qed.