Definition works with implicit arguments but does not work with explicit ones

[slyfr]

The following definition is not accepted by Rocq :

Equations alternate (A:Type) (l1 l2: list A) : list A by wf (length l1 + length l2 ) lt :=
  alternate nil l := l;
  alternate l nil := l;
  alternate (cons x xs) l := cons x (alternate l xs).

but when A is made implicit, everything works fine :

Equations alternate {A:Type} (l1 l2: list A) : list A by wf (length l1 + length l2 ) lt :=
  alternate nil l := l;
  alternate l nil := l;
  alternate (cons x xs) l := cons x (alternate l xs).

I think both should work