  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.
  Along the way, we define a framework for space efficiency, traversing the
design space with three different space-efficient manifest calculi. We examine
the diverse correctness criteria for contract semantics; we conclude with a
coercion-based language whose contracts enjoy (galactically) bounded, sound
space consumption---they are observationally equivalent to the standard,
space-inefficient semantics.
