Ghc.List: size-related properties and termination
Data.Splay: well-ordered trees and termination
Data.Map: binary-search ordered trees and termination
Bytestring: size-based low-level memory safety and termination
Text: size-based pointer-safety and termination