To support a proposed extension of constructor unboxing in OCaml, we need to compute a property of OCaml type expressions by repeatedly unfolding the definition of datatype constructors. In presence of mutually-recursive datatype definitions, it is not obvious to do such repeated unfolding without losing termination. We present an unfolding algorithm using dynamic cycle detection, which is more permissive than the traditional static cycle detection approach.