Anomaly Invalid_argument ("index out of bounds")

[TDiazT]

trafficstars

I came up with this error :

Error:
Anomaly
"Uncaught exception Invalid_argument("index out of bounds")."
Please report at http://coq.inria.fr/bugs/.

I am not sure how to make a simple example replicating the issue :/ .. I have the following structure (more or less):

• A with clause with nothing too fancy.
• A with clause with a nested where clause, in which there are some with clauses over some elements in context (ty).

Equations? foo : T1  -> list T2 -> list (T3 * T4)  by wf (some_measure ...) :=
    {
      foo _ [::] := [::];
      
      foo t (C1 ... :: tl)
        with bar ... :=
        {
        | true := foo t (some_sublist_of_c1 ++ tl);
        | _ := foo t tl
        };

      foo t (hd :: tl)
        with baz t (qux hd _) :=
        {
        | Some ty := ((qux  hd _), nested_foo (quux t (qux hd _)))
                         :: foo t (filter some_predicate tl)

           where nested_foo : option (A + B + list C) -> T4 :=
                   {
                     nested_foo None := ... ;

                     nested_foo (Some (inr vs))
                       with ty :=
                       {
                       | X1 := ... (map (fun ... => recursive_call_to_foo) vs);
                       | _ := ...
                       };

                    nested_foo (Some (inl (inl value))) := ... ;

                    foo (Some (inl (inr v))) := ... recursive_call_to_foo 
                   };

        | _ :=  ... :: foo t (filter some_predicate tl)
        }
    }.

(* qux is basically a function to extract information out of constructors of T2, with a proof that the element was not built with C1 *)

[TDiazT]

I changed the definition so I no longer do that with clause over ty in the nested where clause and I no longer get the error message. I basically lifted that inner check to the with clause over the baz call :

If (ty := X1 | X2),

with baz t (qux hd _) :=
        {
        | Some X1 := ((qux  hd _), nested_foo (quux t (qux hd _)))
                         :: foo t (filter some_predicate tl)

           where nested_foo : option (A + B + list C) -> T4 :=
                   {
                      nested_foo (Some (inr vs)) := ... (map (fun ... => recursive_call_to_foo) vs); (* Removed with clause *)

                      nested_foo _ := ...
                   };

        | Some X2 := ((qux  hd _), nested_foo (quux t (qux hd _)))
                         :: foo t (filter some_predicate tl)

           where nested_foo : option (A + B + list C) -> T4 :=
                   {
                      nested_foo ... := ... ;
                      nested_foo _ := ...
                   };

        | _ :=  ... :: foo t (filter some_predicate tl)
        }

[TDiazT]

I actually get the error in 212 with this new definition 😄.