Comment 11 for bug 942237

Actually, you know what would /almost/ work?

   (defknown unknown-nil () t (flushable))

   (defun unknown-nil () nil)

and expanding the DOLIST in

   (defun foo (strings)
     (let ((n 0))
       (dolist (s strings n)
        (declare (string s))
        (incf n (length s)))))

to

   (BLOCK NIL
     (LET ((#:N-LIST957 STRINGS))
      (TAGBODY
       #:START958
         (UNLESS (ENDP #:N-LIST957)
           (LET* ((S (CAR #:N-LIST957)))
             (DECLARE (STRING S))
             (SETQ #:N-LIST957 (CDR #:N-LIST957))
             (TAGBODY (INCF N (LENGTH S))))
           (GO #:START958))))
     (LET ((S (UNKNOWN-NIL)))
       (DECLARE (IGNORABLE S))
       (DECLARE (STRING S))
       N))

...only issue being that the compiler isn't brave enough to delete S as unused because there's a cast.