VM confused by let bindings in fixpoints

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3282
From: @maximedenes
Reported version: 8.5
CC: @herbelin, @JasonGross

[coqbot]

Comment author: @maximedenes

Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n.

Eval vm_compute in f.

(* returns fix Ffix (x x0 : nat) {struct x} : nat := x0
: nat -> let o := true in nat -> nat *)

(* the struct argument is the wrong one, and so are the reductions )
( This bug is worse than it seems, because it may in theory be exploited to trick the guard checker (cf subterm relation on fixpoints) *)

[coqbot]

Comment author: @JasonGross

Probably related:

Definition foo := fix f (m : nat) (o := true) (n : nat) {struct n} := match n with 0 => 0 | S n' => f 0 n' end.
(* Toplevel input, characters 18-110:
Error:
Recursive definition of f is ill-formed.
In environment
f : forall m : nat, let o := ?3 in nat -> nat
m : nat
n : nat
Not enough abstractions in the definition.
Recursive definition is:
"fun m : nat =>
let o := ?3 in fun n : nat => match n with
| 0 => 0
| S n' => f 0 n'
end".
*)

[coqbot]

Comment author: @herbelin

Both problems are different. Jason's problem is actually the trace of two easy bugs which are now fixed in trunk (1894f56), 8.4 and 8.3.

Maxime's problem is a problem of the vm. I attach a patch but I don't think this is the correct one. Compilation of fix in vm is not taking care of let-in's, and I believe that the unsafe_rec_arg in vm.ml is really doing unsafe things, looking in a block which is not the expected one when the fix has let-ins.

The patch I attach simply expands let-ins instead of compiling them. Unless Benjamin G. is around to look at this, I think, Maxime, that you are the most knowledgeable to know what to do exactly.

Hugo

[coqbot]

Comment author: @herbelin

Created attachment 483
Patch for remaining vm fix with let-in bug.

Attached file: patch-fixpoint-with-let-in-vm (text/plain, 756 bytes)
Description: Patch for remaining vm fix with let-in bug.

[coqbot]

Comment author: @maximedenes

I can take the VM part of this problem, although I will probably not have time to fix it before the POPL deadline.

Expanding let-ins may cause performance issues by loosing sharing, so I'll try to see if we can still support them.

[coqbot]

Comment author: @maximedenes

Fixed in trunk.

[herbelin]

Yet other occurrences of the bug:

Definition foo' := fix f (o := true) {n : nat} p {struct n} :=                                        
  match n with 0 => 0 | S n' => f (n:=n') 0 end.
(*
Recursive definition of f is ill-formed.
Recursive call to f has principal argument equal to "0" instead of "n'".
*)

or, specifically in the 8.11 branch:

Definition foo'' := fix f {m : nat} (o := true) (n : nat) {struct n} :=
  match n with 0 => 0 | S n' => f (m:=0) n' end.
Definition cofoo' := cofix f {m} (o := true) := {| hd := 0; tl := f (m:=0) |}.
(* anomaly: File "interp/impargs.ml", line 361, characters 15-21: Assertion failed. *)

I'm going to submit a short patch.

Also for cofix.