Error: Anomaly "Uncaught exception Equations.Covering.UnfaithfulSplit(_)."

[tyilo]

$  coqc Bug.v
File "./Bug.v", line 23, characters 0-120:
Error: Anomaly "Uncaught exception Equations.Covering.UnfaithfulSplit(_)."
Please report at http://coq.inria.fr/bugs/.

Using coq version 8.9.1 and coq-equations version 1.2.1+8.9.

Contents of Bug.v:

Require Import Equations.Equations.

Inductive vec (A:Type) : nat -> Type :=
  | nil : vec A 0
  | cons : forall n, A -> vec A n -> vec A (S n).

Arguments nil {A}.
Arguments cons {A n}.

Derive Signature for vec.

Notation "x :: v" := (cons x v).
Notation "[ ]" := nil.
Notation "[ x ]" := (cons x nil).
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )).

Equations head {A n} (v : vec A (S n)) : A :=
head (x :: _) := x.

Equations tail {A n} (v : vec A (S n)) : vec A n :=
tail (_ :: v) := v.

Equations vec_vec {A:Type} {n} (v : vec  A n) : vec A n :=
vec_vec _ (n:=?(0)) := [];
vec_vec v := (head v) :: (tail v).

[mattam82]

Ah indeed, you should get an error message telling that 0 cannot be inaccessible here, as vec_vec is really pattern matching on n rather than v.