Equations handles certain overlapping patterns incorrectly.

[ANogin]

The following example:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : foo.

Definition foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List => list unit
  end.

Equations num (f:foo) (val:foo_type f) : nat := {
  num Nat val := val;
  num List val := length val }
(* Using "where" instead of a separate Equations here because of Issue #73 - want to specify explicit (struct ts) here and it only works with "where" *)
where (struct fs) sum (fs : list foo) (val: compact_prod (map foo_type fs)) : nat := {
  sum nil _ := 0;
  sum (cons f nil) val := num f val;
  sum (cons f tl) val := num f (fst val) + sum tl (snd val)}.

results in the following error:

Recursive definition of sum is ill-formed.
In environment
num : forall f : foo, foo_type f -> nat
f : foo
val : foo_type f
sum : forall fs : list foo, compact_prod (map foo_type fs) -> nat
fs : list foo
val0 : compact_prod (map foo_type fs)
f0 : foo
l : list foo
val1 : compact_prod (map foo_type (f0 :: l))
f1 : foo
l0 : list foo
val2 : compact_prod (map foo_type (f0 :: f1 :: l0))
Recursive call to sum has principal argument equal to "f1 :: l0" instead of one of the following variables: 
"l" "l0".
Recursive definition is:
"fun (fs : list foo) (val : compact_prod (map foo_type fs)) => sum_functional num sum fs val".

[ANogin]

I have not fully tested it yet, but so far the following version appears to be compiling without errors, so could be a possible workaround:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : foo.

Definition foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List => list unit
  end.

Equations num (f:foo) (val:foo_type f) : nat := {
  num Nat val := val;
  num List val := length val }.

Equations (struct fs) sum (fs : list foo) (val: compact_prod (map foo_type fs)) : nat := {
  sum nil _ := 0;
  sum (cons f tl) val <= sum tl => {
  sum (cons f nil) val sumtl := num f val;
  sum (cons f _) val sumtl := num f (fst val) + sumtl (snd val)}}.

[mattam82]

Indeed, for this to work you have to capture the "intermediate" tl value somehow, otherwise it gets expanded to a cons and the recursive call cannot be seen to be guarded anymore. There's not much else one can do I think.

[ANogin]

Wouldn't it be possible for Equations to know not to expand the tl in the first place? Is there a reason why it absolutely needs to get expanded?

[mattam82]

Yes it needs too. Otherwise (snd val) wouldn't typecheck, as val would be of type: compact_prod (map foo_type tl) which wouldn't reduce to a cartesian product type.

[ANogin]

Ah, OK, makes sense. So I guess the only automated solution would effectively be to automate my "workaround" transformation, but just using the manual workaround is probably good enough as well (at least, good enough for me, unless this causes some unexpected difficulties in using the definitions that I am not yet aware of - for now, I am still trying to get the definitions themselves to compile, and have not yet tried actually using them in any theorems/proofs).

[mattam82]

I don't think there is much better we can do for now, hence closing.