Cloning function with bad ghost status raises Invalid_argument("Expr.let_rec")
The following fails with anomaly: Invalid_argument("Expr.let_rec")
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
The error message points to the clone
line. Removing the rec
keyword from the definition of ff
, or stating the argument x
, of function f
in module B, as ghost removes the problem.
The error message is a little cryptic, and I don't fully understand why this only happens when we call f
inside a let rec
definition.