Monadic regions
"We offer a typeclass-based implementation of Monadic Regions. Region is a memory allocation technique introduced by Tofte and Talpin and implemented in ML-Kit and Cyclone. A region is an area of memory holding heap allocated data (reference cells). Regions may nest and so more than one region may be active at any given point. A new reference cell may only be allocated in an active region, and may then only be used while that region is active. The system statically guarantees that no cell can be accessed when its region is closed. Therefore, all cells in a region can be immediately garbage collected when the region is closed."
"The code gives the first example of the total type comparison predicate, which can handle even non-ground types and quantified type variables."