The term exhaustiveness checking comes from functional languages, and programmers experienced with functional languages may feel confused — where are the algebraic data types?
In, say, Ocaml, to get exhaustiveness checking, you first have to define an ADT:
type step = Hop | Skip | Jump
This superficially resembles the deftype form above, but what it does is very different. The Ocaml defines new types; but in the Common Lisp version there is no hop, skip, or jump type; they remain just symbols.
(type-of :hop) => KEYWORD
There have been several efforts to bring ADTs into Common Lisp; I am even responsible for one of them. A Lisp equivalent to the Ocaml above:
(defunion step hop skip jump)
(type-of hop) => HOP
But while there are situations where ADTs in CL are very helpful (e.g. compilers) most of the time they are unidiomatic.
By defining types as disjunctions, however, we can take completely idiomatic pieces of Common Lisp, ones that use ad-hoc polymorphism, and add a degree of static safety – exhaustiveness checking – with minimal changes, and without making the code harder for other Lispers to understand.
To speak as the Clojurists do: in the ML family of languages ADTs and exhaustiveness checking (and pattern matching) are complected. But ADTs are useful – even in Haskell, which does not (by default) provide exhaustiveness checking. And exhaustiveness checking is also useful – even without ADTs.
Static safety is not a single axis with C at the bottom and Idris at the top. There are different, orthogonal axes of static safety. Type inference through unification is a form of static safety that ML-family languages provide that Lisp does not. But there are also forms of static safety Lisp offers that MLs do not. Macros are of course the most important; but exhaustiveness checking on type disjunctions is another valuable one.