Error: Anomaly "Not an unfoldable reference."

[JasonGross]

Within the past four days or so (since the merging of #18014), it seems there's been a regression that introduced an anomaly into fiat-crypto-legacy:

File "./src/Experiments/SimplyTypedArithmetic.v", line 7059, characters 4-350:
Error: Anomaly "Not an unfoldable reference."
Please report at http://coq.inria.fr/bugs/.

[JasonGross]

@coqbot minimize coq.dev

git clone --recurse-submodules https://github.com/mit-plv/fiat-crypto.git --branch=sp2019latest
cd fiat-crypto
make TIMED=1 some-early util

[coqbot-app]

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

[SkySkimmer]

Seems to be from #17993

[SkySkimmer]

Reduced

Fixpoint even n := match n with 0 => true | S n => negb (odd n) end
with odd n := match n with 0 => false | S n => negb (even n) end.

Definition boo n (x:unit) := even n.

Eval simpl in boo 2. (* anomaly *)

The problem appears with a partially applied definition whose body is a mutual fixpoint (PartialEvaluate is the partially applied definition in fcl).

cc @herbelin

[herbelin]

Interestingly, the following fails similarly even before #17993:

Fixpoint even n := match n with 0 => fun _ : unit => true | S n => odd n end
with odd n := match n with 0 => fun _ => false | S n => even n end.

Definition boo n (x:unit) := even n x.

Fail Eval simpl in boo 2.
(* Not an unfoldable reference. *)

[herbelin]

Another interesting example (before #17993):

Fixpoint f_fix_fun n := match n with 0 => fun _ : unit => true | S n => fun _ => true end.
Definition boo_fix_fun n := f_fix_fun n.
Eval simpl in boo_fix_fun 2. (* fun _ : unit => true *)

Fixpoint f_fix n := match n with 0 => fun _ : unit => true | S n => fun _ => true end.
Definition boo_fix n := f_fix n tt.
Eval simpl in boo_fix 2. (* boo_fix 2 *)

Definition f_case n := match n with 0 => fun _ : unit => true | S n => fun _ => true end.
Definition boo_case n := f_case n tt.
Eval simpl in boo_case 2. (* true *)

Shouldn't it be consistent, typically by reducing also boo_fix 2 to true? [Added: actually, in the general case, we would not know how to refold such boo_fix, so maybe it is ok.]