OxCaml extends the OCaml type system with \emph{modes} for safe low-level systems programming. For example, OxCaml’s modal \emph{portability} and \emph{contention} axes ensure data-race freedom. In practice, however, modal tracking can reject programs that are obviously safe, such as when the data shared across threads is immutable. To remedy this problem, we introduce \emph{mode crossing}—the ability to automatically strengthen modes (e.g., from nonportable to portable) for values of certain types. Mode crossing significantly reduces the annotation burden associated with modal types. To support mode crossing in the presence of abstract type specifications, we further introduce a new type system feature, \emph{modal kinds}.

We present a type-theoretic account of modal kinds, interpret them as monotone functions on a lattice of modes, and extend this interpretation to recursive and abstract types. We verify soundness in Rocq on top of Iris. We design an inference procedure that reduces kind checking and subsumption to constraints solved by a dedicated lattice solver. Our design is implemented in the OxCaml compiler and deployed in a large industrial codebase, demonstrating practical usability.