Merge PR #7521: Fix soundness bug with VM/native and cofixpoints

1 files changed, 5 insertions, 1 deletions

diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 4a3c03d85e..f42c46175c 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -31,7 +31,7 @@ and lambda =
   | Lprim         of pconstant * int (* arity *) * instruction * lambda array
   | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
   | Lfix          of (int array * int) * fix_decl
-  | Lcofix        of int * fix_decl
+  | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
   | Lmakeblock    of int * lambda array
   | Lval          of structured_constant
   | Lsort         of Sorts.t
@@ -39,6 +39,10 @@ and lambda =
   | Lproj         of int * Constant.t * lambda
   | Luint         of uint
 
+(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
+to be correct. Otherwise, memoization of previous evaluations will be applied
+again to extra arguments (see #7333). *)
+
 and lam_branches =
   { constant_branches : lambda array;
     nonconstant_branches : (Name.t array * lambda) array }