> Is that the type of FOO or the return type of FOO?
It is the type of FOO, it reads as: a function which takes one argument of any type (T) and returns exactly one value, which is either 42 or a string of length 9.
Another example:
(defun xyz (x y z)
(declare (type fixnum x)
(type float y)
(type (vector (unsigned-byte 8) 1024) z))
(aref z (+ x (round y))))
(FUNCTION
(FIXNUM FLOAT (VECTOR (UNSIGNED-BYTE 8) 1024))
(VALUES (UNSIGNED-BYTE 8) &OPTIONAL))
Here there are three arguments, the third one being a vector of bytes of length 1024. Note that the return values was inferred from the inputs.
> This is no exception, however it seems that this inferencer is useful primarily for enabling compiler optimizations rather than for performing type checking. Is that correct?
It is a mix of both, really.
CL is primarily designed to be dynamic. Static analyses are used to optimize code and prevent classes of errors if they can be detected in advance. If you define detecting a type error as a positive test, then SBCL allows to have false negatives. That happens in cases where the expected and actual types overlap: there might be an error, or not, so the actual check is delegated at runtime.
Another thing is that with global functions (defun), it seems that there is some widening happening, for the return type in particular, so that (OR INTEGER STRING) is treated as T. This does not happen with inline or local functions. Note also that global functions can be called from anywhere, be redefined (except standard ones) and they are generally responsible for checking their arguments, except when you explicitely turn the safety knob down and add type declarations.
So let's say that XYZ above is declared to be inlined, and we use it as follows:
(defun use-xyz-1 (x y z)
(declare (type positive-float y)
(type (integer 0 3000) x))
(xyz x y z))
The above is compiled without problems, even though you could give values which would make an out-of-bounds access. However, you will surely agree that there are theoretical limits to static type checking, so it is expected that not all expressions can be typed in CL as precisely as you could wish (of course, going up the lattice, functions accept type T arguments). However, when you change type declarations so that the intersection of expected/actual types is empty:
(defun use-xyz-2 (x y z)
(declare (type positive-float y)
(type (integer 2000 3000) x))
(xyz x y z))
... the compiler warns you that:
;; Derived type (INTEGER 2000 4611686018427387900) is not a suitable
;; index for (VECTOR (UNSIGNED-BYTE 8) 1024)
The way SBCL treats declaration is that they are used as assertions (except for return types in global declarations, see manual).
So what does it mean to treat declaration as assertions? Here is FOO:
(defun foo (float)
(make-string (abs (ceiling float)) :initial-element #\#))
It makes a new string made of N times character "#", where N is computed from the float input. Then, we call FOO from BAR:
(defun bar (x)
(foo x)
(typecase x
(float 0)
(integer 1)
(t 2)))
The unique value returned by BAR is of type `(integer 0 0)`, because knowing that `(foo x)` succeeds allows us to conclude that X was indeed a FLOAT, and thus the TYPECASE expression necessarily returns zero. Declarations, assertions, etc. can be used by the compiler.
Note that the equivalent (w.r.t. return value) function below has a different type:
(defun bar (x)
(prog1
(typecase x
(float 0)
(integer 1)
(t 2))
(foo x)))
This time, the return type is (MOD 3), i.e. the set {0,1,2}, even though propagation could be applied backward. However, backward propagation seems to pose problem w.r.t. the CL standard, at least that's what is said here (a good reference, by the way):
https://www.pvk.ca/Blog/2013/04/13/starting-to-hack-on-sbcl/
Static typing in SBCL gives something I did not yet witness in other languages. I defined a state machine with local functions, roughly as follows:
(defun sm ()
(let ((state))
(labels ((a () (setf state #'b))
(b () (setf state #'c))
(c () (if (plusp (random 2))
(setf state #'d)
(setf state #'b)))
(d () (setf state #'a))
(e () (return-from sm)))
(loop (funcall state)))))
So the local variable "state" holds current function. And so, this compiles (and the actual, longer code did so as well) with a note saying "deleting unused function (LABELS E :IN SM)", because "state" is known to never reach E. By the way, function SM never returns normally, as explained by the NIL return type. That was a useful and unexpected thing to notice.