> Consider an identity function declared to only accept fixnums and returns fixnums. If you call this function with a string a type error will be signaled if run time type checks are enabled.

This would be the case that I referred to in the second paragraph of my last comment. I would agree if we were talking about explicit type checks, but a portable Common Lisp program cannot consider implicit added by the compiler to be part of the programs semantics, because a compliant implementation is not required to add any type checks. SBCL just adds them as a debugging aid, but if you rely on type errors being signaled, you have to check them explicitly with `CHECK-TYPE` or something equivalent.

> Think of soundness as a guarantee that if the program type checks

This would be where our view is different. You consider soundness to be a guarantee given by the compiler, while I consider it a property of the program itself (which can sometimes be checked by the compiler, and sometimes by the programmer). Common Lisp does not give any guarantee of type safety. SBCL simply tries to be helpful and catch most real world type errors, but ultimately it is the programmer who must ensure the soundness of the program.