Depending on what you allow in predicate types, you end up making type inference (and/or type checking) an undecidable problem. In Common Lisp, you can write

Depending on what you allow in predicate types, you end up making type inference (and/or type checking) an undecidable problem. In Common Lisp, you can write (deftype element () `(integer 100 1000)) and in this case, a "smart" compiler like SBCL will be able to infer the bounds of (the element x), but for more complex predicates, like (deftype even-element () `(and (integer 100 1000) (satisfies evenp))) I highly doubt there is a single CL compiler out there that'd be able to e.g. optimize (logand 1 (the even-element x)) into the constant 0. Thus declaring types like this -- in Common Lisp at least -- is only really useful for documenting code and run-time validation.