It would be nice if SBCL in particular could be made to adopt this use of types.

I agree, that would be an easy extension (at least from the user-facing API PoV) and would tremendously improve the language!

The only difference between static and runtime typing would be the stage at which the types are evaluated, and being the same as macros they might be more interesting in that regard since they might have to consider what it means to run at both stages of evaluation.

That is the only difference, but that difference has important consequences on optimization.