But now "f" is entirely monomorphic (rather than just having an automatic specialization for float), AFACIT.
Read Henry Baker's paper on the CL-84 type inference engine. The intellectual ancestor of all modern dynamic PL optimization.
I'm not really famililar with CL, so forgive the perhaps dumb question: Does what you mentioned permit the user to write the completely generic algorithm while guaranteeing that it'll be specialized/monomorphized automatically by the comiler/runtime[1] when possible? As understood it, the thing the PP cared about whether it was guaranteed to occur and that it be automatic.
(I'm aware that these checks can be made very cheap, like JIT compilers do, but they're not zero-cost like compile-time monomorphization would be.)
[1] I mean if you want to avoid segfaults w/e.g. "No type checks".
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.