Suppose that we have some function
let rec f x y = ... (f z) ...
and we want to ensure that all the closures
f v (whatever
v) have a uniquely recognizable code pointer (word 0 of the block). In particular, the above does not work because the code pointer will point to something extremely common like
caml_apply (or whatever it is called).
We could go for the following
let [@inline never] rec f x = (); fun y -> ... (f z) ...
but there are some concerns that Flambda breaks the “
So, what would be a foolproof way to do that?
(For more context, this comes from an attempt at getting rid of naked pointers in Coq.)