CHECK-TYPE doesn't allow optimization in all cases?

[Attila Lendvai]

try to compile this definition with all the combination of the commented out 'check-type and 'declare type (none, both, etc).

all the compilations will result in a different number of optimization notes, which suggests that the two different ways of communicating the type information to the compiler does not result in the same type annotation.

strictly speaking this is not a bug, but i prefer using 'check-type to 'declare for the guaranteed error it signals, and i'd also like to have the same optimizations applied in that case.

i've tried to reduce the test case, but the difference goes away even with small changes...

this is with 1.0.32.37 on x86_64.

(in-package :cl-user)

(defun write-ratio-as-floating-point (number stream digit-length-limit)
  (declare (optimize speed))
  ;(declare (type fixnum digit-length-limit))
  ;(check-type digit-length-limit fixnum)
  (flet ((fail ()
           (unless *silently-truncate-ratios*
             (with-simple-restart (continue "Disable this check globally and ignore precision loss silently in upcoming such situations")
               (error 'database-error :message
                      (format nil "Can not write the rational ~A with only ~A digits. You may want to (setf ~S t) if you don't mind the loss of precision."
                              number digit-length-limit '*silently-truncate-ratios*)))
             (setf *silently-truncate-ratios* t))))
    (multiple-value-bind (quotient remainder)
        (truncate (if (< number 0)
                      (progn
                        (write-char #\- stream)
                        (- number))
                      number))
      (let* ((quotient-part (princ-to-string quotient))
             (remaining-digit-length (- digit-length-limit (length quotient-part))))
        (write-string quotient-part stream)
        (when (<= remaining-digit-length 0)
          (fail))
        (unless (zerop remainder)
          (write-char #\. stream))
        (loop :for decimal-digits :upfrom 1 :until (zerop remainder)
              :do (when (> decimal-digits remaining-digit-length)
                    (fail))
              :do (multiple-value-bind (quotient rem) (floor (* remainder 10))
                    (princ quotient stream)
                    (setf remainder rem)))))))

[Tobias C. Rittweiler (tcr)]

I don't get any notes at all with 1.0.33.2 on x86-32. Perhaps you can add the actual notes
for both cases.

[Nikodemus Siivola (nikodemus)]

  status confirmed
  tag optimization compiler
  importance low
  summary "CHECK-TYPE doesn't allow optimization in all cases?"
  done

CHECK-TYPE and DECLARE are really quite different -- that is to be expected. That said, all is not as it should be. With just CHECK-TYPE I get among other things

; (- DIGIT-LENGTH-LIMIT (LENGTH QUOTIENT-PART))
;
; note: forced to do GENERIC-- (cost 10)
; unable to do inline fixnum arithmetic (cost 2) because:
; The first argument is a T, not a FIXNUM.
; The result is a (VALUES NUMBER &OPTIONAL), not a (VALUES FIXNUM &REST T)

where the compiler should certainly be able to tell that the first argument is indeed a fixnum.

Haven't looked into why yet.

[Alexey Dejneka (adejneka)]

DIGIT-LENGTH-LIMIT is a closed-over variable in FAIL. SBCL constraint propagator does not consider local function calls (except for LET calls) to be control transfers and so does not see that CHECK-TYPE in WRITE-RATIO-AS-FLOATING-POINT dominates usage of DIGIT-LENGTH-LIMIT inside FAIL.

[3b (00003b)]

simpler test case of what seems to be the same problem, on "1.3.11.17-0c8ef9f" x8664

(defun foo (x)
  (declare (optimize speed))
  (check-type x single-float)
  (progn ;locally (declare (single-float x))
   (flet ((y () (+ 1.0 x)))
     (list (y) (y)))))

; in: DEFUN FOO
; (+ 1.0 X)
;
; note: forced to do GENERIC-+ (cost 10)
; unable to do inline float arithmetic (cost 2) because:
; The first argument is a T, not a SINGLE-FLOAT.
; The result is a (VALUES NUMBER &OPTIONAL), not a (VALUES SINGLE-FLOAT
; &REST T).
; unable to do inline float arithmetic (cost 3) because:
; The first argument is a T, not a (COMPLEX SINGLE-FLOAT).
; The result is a (VALUES NUMBER &OPTIONAL), not a (VALUES
; (COMPLEX SINGLE-FLOAT)
; &REST T).

with the LOCALLY instead of PROGN, there are no notes