Ill-typed term produced after name collision (?)

[Armael]

In the example below (tested with Coq 8.19+Equations 1.3+8.19 and Coq 8.20+Equations 1.3.1+8.20), Equations generates an ill-typed term for the second clause. The example can be made to work by renaming a1 into ar1, which hints at a name collision issue.

More precisely, the name clash seems to be with the a implicit parameters of G, Y, R in regularity: renaming this a into something else also makes the code work.

From Equations Require Import Equations.

Axiom push6 : forall {A} (a1 a2 a3 a4 a5 a6 : A),
  unit.

Inductive stored (A : Type) (l : nat) : Type :=
  | Stored.

Definition six_stored (A : Type) (l : nat) : Type :=
  stored A l * stored A l * stored A l *
  stored A l * stored A l * stored A l.

Inductive green_hue  := SomeGreen  | NoGreen.
Inductive yellow_hue := SomeYellow | NoYellow.
Inductive orange_hue := SomeOrange | NoOrange.
Inductive red_hue    := SomeRed    | NoRed.

Inductive color :=
  Mix : green_hue -> yellow_hue -> orange_hue -> red_hue -> color.

Notation green := (Mix SomeGreen NoYellow NoOrange NoRed).
Notation yellow := (Mix NoGreen SomeYellow NoOrange NoRed).
Notation red := (Mix NoGreen NoYellow NoOrange SomeRed).

Inductive regularity : color -> color -> nat -> color -> color -> Type :=
 | G {a Cl rC} : regularity green  green a      Cl    rC
 | Y {a Cl rC} : regularity yellow Cl    (S a)  Cl    rC
 | R {a}       : regularity red    red   (S a)  green green.

Inductive kind : Type := only | left | right.

Inductive triple : Type -> nat -> kind -> color -> Type :=
  | Triple {A : Type} {l : nat} {a : nat}
           {k : kind} {C lC rC Cpkt : color} :
    regularity C Cpkt a lC rC ->
    triple A l k Cpkt.

Equations only_of_right {A lvl C}
  (six : six_stored A lvl)
  (tr : triple A lvl right C)
:
  unit :=
only_of_right (a1, a2, a3, a4, a5, a6) (Triple G) := tt;
(* BUG: ill-typed term. Renaming a1 into ar1 below makes the code work. *)
only_of_right (a1, ar2, ar3, ar4, ar5, ar6) _
  with push6 a1 ar2 ar3 ar4 ar5 ar6 => { | _ := tt }.