Even in statically typed languages it is useful to have certain
invariants checked dynamically.  Findler and Felleisen gave an
algorithm for dynamically checking expressive higher-order types
called contracts.  If we postulate soundness (in the sense that no
well-typed term will ever be blamed as being ill-typed), then their
algorithm implies a semantics for types.  Unfortunately, the implicit
nature of the resulting model makes it rather unwieldy.
  
In this paper we demonstrate that a direct approach yields essentially
the same semantics without having to mention the contract checking
algorithm at all.  The so-defined model largely coincides with
intuition, but it does expose some peculiarities in its interpretation
of predicate types.  In fact, a particularly naive but appealing
interpretation of such types would have resulted in loss of soundness.
The interpretation used in our model draws upon the notion of safety.
  
We also show that counter-intuitive aspects of the semantics can be
avoided if we are willing to change the language of types.  The
corresponding loss in expressive power can be recovered by extending
the type language in a way that (either in ad-hoc fashion or, e.g., by
including general recursive types) makes it possible to explicitly
express safety as a type.