Type propagation problem on SBCL

type-propagation.lisp

;;; A difference between DECLARE TYPE and CHECK-TYPE produces an
;;; optimization problem on SBCL.

(declaim (inline add-with-declaring-type!))
(defun add-with-declaring-type! (vector1 vector2)
  (declare (vector vector1 vector2))
  (loop for idx below (length vector1)
        do (incf (aref vector1 idx) (aref vector2 idx))
        finally (return vector1)))

(declaim (inline add-with-checking-type!))
(defun add-with-checking-type! (vector1 vector2)
  (check-type vector1 vector)
  (check-type vector2 vector)
  (loop for idx below (length vector1)
        do (incf (aref vector1 idx) (aref vector2 idx))
        finally (return vector1)))

(defun test ()
  (declare (optimize (speed 3) (safety 1)))
  (let ((vec (make-array 5 :element-type 'fixnum)))
    ;; Type (SIMPLE-ARRAY FIXNUM (10)) is successfully propagated into the inlined code.
    (add-with-declaring-type! vec vec))
  (let ((vec (make-array 10 :element-type 'fixnum)))
    ;; Optimization fails because the type information is superseded by VECTOR.
    (add-with-checking-type! vec vec)))

;;;
;;; Workaround
;;;

(defmacro check-type* (place type &optional type-string &environment env)
  "A variant of SBCL's CHECK-TYPE (tweaked at the suggestion of g000001).
See https://g000001.cddddr.org/3619219980"
  (declare (ignorable env))
  #+sbcl
  (let ((expanded (sb-impl::%macroexpand place env)))
    (if (symbolp expanded)
        `(do ()
             ((typep ,place ',type))
           (setf (the ,type ,place) (sb-kernel:check-type-error ',place ,place ',type
                                                                ,@(and type-string
                                                                       `(,type-string)))))
        (let ((value (gensym)))
          `(do ((,value ,place ,place))
               ((typep ,value ',type))
             (setf (the ,type ,place) (sb-kernel:check-type-error ',place ,value ',type
                                                                  ,@(and type-string
                                                                         `(,type-string))))))))
  #-sbcl `(check-type ,place ,type ,type-string))

(declaim (inline add-with-checking-type*!))
(defun add-with-checking-type*! (vector1 vector2)
  (check-type* vector1 vector)
  (check-type* vector2 vector)
  (loop for idx below (length vector1)
        do (incf (aref vector1 idx) (aref vector2 idx))
        finally (return vector1)))

(defun test2 ()
  (declare (optimize (speed 3) (safety 1)))
  (let ((vec (make-array 10 :element-type 'fixnum)))
    ;; This time optimization succeeds.
    (add-with-checking-type*! vec vec)))