simp not working - foo_type_equation_1 fails with "Cannot refine with term ... because a metavariable has several occurrences."

[ANogin]

Using the recent v8.8, in the following code

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 :=
| List : list foo -> foo.

Equations foo_type (f:foo) : Type :=
  foo_type (List fs) := compact_prod (map foo_type fs).

Equations num (f:foo) : forall (val:foo_type f), nat := {
  num (List nil) := fun val => 0;
  num (List (cons hd tl)) := fun val => sum hd (num hd) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (num hd) tl (snd val)}.

Lemma num_zero: forall (f:foo) (val:foo_type f), num f val = 0.
Proof.
intro. induction f. simp foo_type in *.

foo_type (List l) is not reduced - and if I try rewrite foo_type_equation_1, it fails with

Cannot refine with term
 "eq_ind_r (fun _ : Type => forall val : foo_type (List l), num (List l) val = 0) ?M2368
    (foo_type_equation_1 ?M2364)"
because a metavariable has several occurrences.

[mattam82]

That's an error of Coq not Equations. One cannot rewrite in a dependent product domain type like this. For example, ssreflect's rewrite rightly complains with:

Dependent type error in rewrite of (fun _pattern_value_ : Type => forall val : _pattern_value_, num (List l) val = 0)

However you can set Transparent foo_type and use simpl with it.