Uncaught exception Failure("List.chop") in equations

[JulesViennotFranca]

Description of the problem

I'm trying to define a recursive function on a mutually recursive types. To do so, I precise a decreasing arguments, but when checking, I get the error :
Anomaly "Uncaught exception Failure("List.chop")." Please report at http://coq.inria.fr/bugs/.

Small Coq file to reproduce the bug

From Coq Require Import ssreflect.
From Coq Require Import Program List Lia.
Import ListNotations.
From Equations Require Import Equations.

Inductive deque (A: Type) : Type := .
Axiom deque_seq : forall {A}, deque A -> list A.

Inductive suffix (A : Type) : Type := 
  | Suff : deque A -> suffix A.

Inductive prefix (A : Type) : Type := 
  | Pre2 : A -> A -> prefix A 
  | Pre3 : A -> A -> A -> prefix A 
  | Pre4 : A -> A -> A -> A -> deque A -> prefix A.
      
Inductive element (A : Type) : nat -> nat -> Type := 
  | ZElt {dpt : nat} : A -> element A 0 dpt
  | SElt {lvl dpt : nat} : 
      prefix (element A lvl dpt) -> 
      lvl_csteque A (S lvl) dpt -> 
      element A (S lvl) (S dpt)

with lvl_packet (A : Type) : nat -> nat -> nat -> Type := 
  | Hole {lvl dpt : nat} : lvl_packet A lvl 0 dpt 
  | Triple {lvl len dpt : nat} : 
      prefix (element A lvl dpt) -> 
      lvl_packet A (S lvl) len dpt ->
      suffix (element A lvl dpt) ->
      lvl_packet A lvl (S len) (S dpt)

with lvl_csteque (A : Type) : nat -> nat -> Type := 
  | Small {lvl dpt : nat} : 
      suffix (element A lvl dpt) -> 
      lvl_csteque A lvl (S dpt) 
  | Big {lvl len dpt nlvl : nat} :
      lvl_packet A lvl len dpt ->
      lvl_csteque A nlvl dpt ->
      nlvl = len + lvl ->
      lvl_csteque A lvl (S (len + dpt)).
    
Arguments ZElt {A}.
Arguments SElt {A lvl dpt}.
Arguments Hole {A lvl dpt}.
Arguments Triple {A lvl len dpt}.
Arguments Small {A lvl dpt}.
Arguments Big {A lvl len dpt nlvl}.

Set Equations Transparent.

Equations suffix_seq {A} : suffix A -> list A := 
suffix_seq (Suff d) := deque_seq d.

Equations prefix_seq {A} : prefix A -> list A := 
prefix_seq (Pre2 a b) := [a] ++ [b];
prefix_seq (Pre3 a b c) := [a] ++ [b] ++ [c];
prefix_seq (Pre4 a b c d e) := [a] ++ [b] ++ [c] ++ [d] ++ deque_seq e.

Equations map_concat {A B : Type} (f : A -> list B) (l : list A) : list B := 
map_concat f [] := [];
map_concat f (a :: l) := f a ++ map_concat f l.

Inductive seq_kind : Type := Element | FPacket | RPacket | CSteque.

Equations? structure_seq {A} (lvl len dpt : nat) (k : seq_kind)
    (elt : match k with 
    | Element => element A lvl dpt 
    | FPacket | RPacket => lvl_packet A lvl len dpt 
    | CSteque => lvl_csteque A lvl dpt
    end) : list A by wf (lvl + len + dpt) lt := 
structure_seq 0 len dpt Element (ZElt a) := [a];
structure_seq (S lvl) len (S dpt) Element (SElt p cs) := 
    map_concat (structure_seq lvl len dpt Element) (prefix_seq p) ++
    structure_seq (S lvl) len dpt CSteque cs;
structure_seq lvl 0 dpt FPacket Hole := [];
structure_seq lvl (S len) (S dpt) FPacket (Triple p pkt _) := 
    map_concat (structure_seq lvl len dpt Element) (prefix_seq p) ++   
    structure_seq (S lvl) len dpt FPacket pkt;
structure_seq lvl 0 dpt RPacket Hole := [];
structure_seq lvl (S len) (S dpt) RPacket (Triple _ pkt s) :=
    structure_seq (S lvl) len dpt RPacket pkt ++
    map_concat (structure_seq lvl len dpt Element) (suffix_seq s);
structure_seq lvl len (S dpt) CSteque (Small s) := 
    map_concat (structure_seq lvl len dpt Element) (suffix_seq s);
structure_seq lvl nlen ndpt CSteque (Big pkt cs eq_refl) := 
    structure_seq lvl _ _ FPacket pkt ++
    structure_seq _ nlen _ CSteque cs ++
    structure_seq lvl _ _ RPacket pkt.

Version of Coq where this bug occurs

8.18.0

Last version of Coq where the bug did not occur

No response

[SkySkimmer]

Seems like an equations bug more than a coq bug
cc @mattam82

[SkySkimmer]

Please reopen at https://github.com/mattam82/Coq-Equations/