Compile-time monomorphization happens only when you request it from the compiler, because it relies on the unsafe assumption that your code won't be redefined.
Common Lisp is designed to be dynamic and the code that is produced should be able to work values of type T (anything) and dispatch it to the correct specific code. SBCL performs static analysis but the only useful way of doing static typing is to assume that known types won't change, otherwise you are going to widen types quickly and treat everything as type T.
The compiler can avoid doing redundant checks, in all modes.
But it is allowed to blindly trust static analysis only if you allow it, because that's a dangerous thing to do. SBCL also has a special operator name TRULY-THE, a more aggressive version of THE (http://clhs.lisp.se/Body/s_the.htm), which declares that an expression is of some type U (e.g. (the single-float x)).
Its use is reserved for cases where you really know what you are doing.
Is static typing as done here useless? Not at all, because sometimes you know that values cannot be redefined, for example inside a function.
I was writing a state machine, with local functions being used as states and a local variable that would be set to the function that represents current state. At one point, I compiled the code and I had a note about code removal being performed. The compiler guessed, based on the different `(setf state ...)` expression, the range of possible values for the state variable and determined that one state was not reachable. This is the kind of things for which the type system is useful, and dead-code elimination was safe to perform here because everything was done in the scope of a single function.