Of course you can invoke a type checker inside a language with compile time macros. Did anyone ever doubt that?
The interesting question is: what does that type checker actually check? How does it deal with normal lisp functions? How is non-trivial data represented? And what happens when it stumbles upon a runtime macro?
And, on a more practical side, how does it access the environment?
This article is more about taking an existing type-checking system (http://www.sbcl.org/manual/#Handling-of-Types) and adding some syntactic sugar so you can declare the types inline, similar to other languages, instead of separately.
The type checker checks types. SBCL's type inference is based on Kaplan-Ullman, rather than Hindley-Milner (see https://news.ycombinator.com/item?id=12216701). A remark from the linked paper there to keep in mind: "There has been some confusion about the difference between type checking for the purposes of compiling traditional languages, and type checking for the purposes of ensuring a program's correctness."
The big caveat with this post is that while types and type declarations are part of the standard, doing what SBCL does to infer them beyond what's declared or handle them for purposes of compile-time warnings and optimized assembly code generation is up to a Common Lisp implementation and others that aren't SBCL (or older SBCL versions, or programs that declare things like (safety 0) to turn off type checks) may behave differently.
Normal lisp functions can have more restrictive types than T, too. Typing (describe 'symbol) for a function will have SBCL say (among other things) that the symbol names a compiled function with a certain argument list, declared type, and derived type. (There's a distinction because I might have declared the function parameter a to be type (integer 0 255) which SBCL simplifies to (unsigned-byte 8).) SBCL has a convenient way to get the derived type info as a list that might be useful for macros or editor extensions, it works for your functions or standard functions e.g. the standard string-to-uppercase function as provided by SBCL has the type: (sb-introspect:function-type #'string-upcase)
i.e. it takes a string (among other possibilities), some optional non-negative integer keyword parameters (up to some max number, which is 2 smaller than my system's most-positive-fixnum value), and outputs a simple-string. This might lead to developing an interesting IDE tool / slime extension that lets you "tab complete" a variable by asking the system what functions you can call that expect the type of the variable's value as the first argument. (slime basically already has this with "who specializes" for finding generic functions.)
You can define your own types with (deftype) for non-trivial data. (Or even trivial data like an enum type: (deftype valid-color () `(member :red :green :blue)) Depending on how non-trivial it is, this may impair optimization opportunities or the compiler being able to notice type mismatches (though you can tell the compiler to give you a notice about type uncertainties), so you're back to runtime checking.
Runtime macros talk to the compiler to generate code, same as compile-time macros. The compiler never goes away in runtime (without some effort in extracting it from the final deliverable anyway) -- COMPILE is a standard compiled function -- which makes it possible to e.g. interactively debug an erroring function, recompile a fixed version that everything will now call instead, all from 100 million miles away back on earth.
A fexpr (funny expression) is a runtime macro. It is a funcall where the arguments are evaluated at runtime not compile time. picolisp, newlisp, and I think lisp 1.5 had fexprs.
The interesting question is: what does that type checker actually check? How does it deal with normal lisp functions? How is non-trivial data represented? And what happens when it stumbles upon a runtime macro?
And, on a more practical side, how does it access the environment?