Typing

Many languages such as Java and C use what is known as strong or static variable typing. This means that when you declare a variable in your application code you must define the variable type.

>>29
I've copied that example expansion straight out of CLHS, however it seems you are right, the CLHS says that it estabilishes that restart, and looking at the implementation of CHECK-TYPE in SBCL, this is what they use signal the error and establish the restart:

(defun check-type-error (place place-value type type-string)
  (let ((condition
         (make-condition
          'simple-type-error
          :datum place-value
          :expected-type type
          :format-control
          "The value of ~S is ~S, which is not ~:[of type ~S~;~:*~A~]."
          :format-arguments (list place place-value type-string type))))
    (restart-case (error condition)
      (store-value (value)
        :report (lambda (stream)
                  (format stream "Supply a new value for ~S." place))
        :interactive read-evaluated-form
        value))))
An actual CHECK-TYPE instance would expand to a DO loop which calls that function I pasted until the type is correct (or the code exits non-locally).