We have found an interesting connection between a type universe hierarchy, à la dependent type theory, and Kripke worlds, used in possible-worlds models of mutable references. We find that type universes are a lightweight syntactic mechanism to design and restrict heap shapes. We extend on this idea and discuss whether type universes are a promising alternative to region type-and-effect systems for static memory management.