Bug with not fully applied term: Anomaly "Uncaught exception Failure("List.chop")"

[thomas-lamiaux]

I have found at least two examples where it returns the anomaly "List.chop" when something is not fully applied

A minimal example where not all variables have been given:

Equations? f x y : _ by wf x lt := f x y := f x.

or

Equations? f x y : _ by wf x _ := f x := f x.

Assume given RoseTree, a size function on it, and an equality test on list:

Section Map_in.
  Context {A : Type}.

  Inductive RoseTree : Type :=
  | leaf : A -> RoseTree
  | node : list RoseTree -> RoseTree.

  Equations sizeRT (t : RoseTree) : nat :=
  sizeRT (leaf a) := 1;
  sizeRT (node l) := 1 + (fold_right Nat.add 0 (map sizeRT l)).

  Equations eqList {X} (eq : X -> X -> bool) (l l' : list X) : bool :=
  eqList eq [] [] := true;
  eqList eq (a::l) (a'::l') := andb (eq a a') (eqList eq l l');
  eqList eq _ _ := false.

then if eqRt is not fully applied in the nesting it returns an anomaly, i.e., this fails

  Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt :=
  eqRT eq (leaf a) (leaf a') := eq a a';
  eqRT eq (node l) (node l') := eqList (eqRT eq ) l l';
  eqRT eq _ _ := false.

but this work

Equations? eqRT (eq : A -> A -> bool) (t t': RoseTree) : bool by wf (sizeRT t) lt :=
eqRT eq (leaf a) (leaf a') := eq a a';
eqRT eq (node l) (node l') := eqList (fun l l' => eqRT eq l l') l l';
eqRT eq _ _ := false.