Space-efficient manifest contracts

The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types - contracts mediating untyped and typed code - is well studied, sound space efficiency for manifest contracts - contracts that check stronger properties than simple types, e.g., "is a natural" instead of "is an integer" - remains an open problem. We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior.