Statically enforcing safe resource management is challenging due to tensions between flexible lifetime disciplines and expressive sharing patterns. Region-based systems [Grossman et al . 2002; Tofte et al . 2001] offer lexically scoped regions under a stack discipline, wherein resources can form arbitrary topology and are managed in bulk. However, they are second-class, can neither escape the scope nor be freely returned. Ownership and linear type systems, such as Rust [Clarke et al. 2013], offer first-class, non-lexical lifetimes with robust static guarantees, but rely on invariants that limit higher-order patterns and expressive sharing.

In this work, we propose a type system that uniformly treats all heap-allocated resources under diverse lifetime, granularity, and sharing settings. Our system provides programmers with three allocation modes: (1) fresh allocation for first-class, non-lexical resources; (2) fresh allocation for second-class resources with lexically bounded lifetimes; and (3) coallocation that groups resources by shadow arenas for bulk tracking and deallocation. Regardless of mode, resources are represented uniformly at the type level, supporting generic abstraction and preserving the higher-order parametric nature of the language.

Obtaining static safety in higher-order languages with flexible sharing is nontrivial. To address this, our solution builds on reachability types [Wei et al . 2024], and our extension adds the capability to track both individual and grouped resources, enables the expression of cyclic store structures, and allows the selective enforcing of stack lifetime discipline. These mechanisms yield $A^q_{<:}$ and ${A}^q_{<:}$ atop, both formalized and proven type safe and memory safe in Rocq.