With the disclaimer that cl:satisfies makes the tun-time type-system turing complete (and no implementation I know of chacks cl:satisfies at compile time), the compiler-available types are strictly non-recursive.<p>For example, you cannot define a type that means "A List of type X" because that requires recursion i.e. this is not allowed:<p><pre><code> (deftype typed-list (x) `(cons ,x (or (typed-list ,x) null)))
</code></pre>
So one must either declare the type of the loop-local variable(s) (when iterating) or the first N item(s) of a list (when recursing), which is a bit unfortunate. SBCL, in particular, does a great job of inferring types at compile time with just a few annotations, but code that is optimizer-friendly is made significantly more ugly by this. Or, you know, people just end up using arrays for everything.