Sure. Consider the type

    forall a. a

With mild conditions on what the program fragment achieving this type can do I can be certain that this function does not return. It is an error, an infinite loop, or simply does not exist.

No contract can verify this because they inspect the value and thus get stuck by infinite loops.

I don't use that sort of thing often, but here's a simpler one:

    sort :: Ord a => [a] -> [a]

I know that `sort` only uses the ordering properties of the values within the list. It could be generalized to `forall a . (a -> a -> Ordering) -> [a] -> [a]` in which case it would be totally oblivious to the values inside of the list except in that it probably applies that function.

No contract system can examine functions. No contract system can prove universals. Types can do both (in certain, principled ways).

---

Another interesting example is handling something like a channel. In Haskell, we have the type `TChan a` which is a channel carrying values of type `a`. In Clojure, the best we can do for giving a contract to a core.async chan is to say it's a "chan containing something" or even "a dereffable thing returning something". To use a contract here we'd have to check every value that ever pops off the channel.

Contracts check shape, but cannot ensure usage.