In this work I will present a new feature proposed for the OCaml programming language, “constructor unboxing”, first suggested by Jeremy Yallop in March 2020. It enables a more efficient representation of certain sum types, but requires a static analysis to forbid certain unboxing requests that would be unsound.

To define this static analysis, one has to solve a problem of normalization of first-order definitions in presence of recursion. In the talk I hope to explain my current understanding of this halting problem, and present an algorithm to compute normal forms and reject (in finite time) non-normalizable definitions.