In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures.

We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander et al. (2008), and show that it can be(right-to-left) directed into an algorithmic check in a surprisingly simple way.

Our implementation of this new check replaced the existing check used by OCaml, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language acquired new features such as GADTs that have subtle interactions with value recursion.