  Standard higher-order contract monitoring breaks tail recursion and leads to
space leaks that can change a program's asymptotic complexity; space-efficiency
restores tail recursion and bounds the amount of space used by contracts.
Space-efficient contract monitoring for contracts enforcing simple type
disciplines (a/k/a gradual typing) is well studied. Prior work establishes a
space-efficient semantics for manifest contracts without dependency (Greenberg
2015); we adapt that work to a latent calculus with dependency. We guarantee
space efficiency when no dependency is used; we cannot generally guarantee
space efficiency when dependency is used, but instead offer a framework for
making such programs space efficient on a case-by-case basis.
