Global FTYPE declarations vs local TYPE declarations

Given the following code:

(defpackage :example
  (:use :cl))

(in-package :example)

(declaim (ftype (function (float float) float) foo1))
(defun foo1 (a b)
  (+ a b))

(defun foo2 (a b)
  (declare (type float a b))
  (the float (+ a b)))

CCL compiles FOO1 to:

    (recover-fn-from-rip)                   ;     [0]
    (cmpl ($ 16) (% nargs))                 ;     [7]
    (jne L65)                               ;    [10]
    (pushq (% rbp))                         ;    [12]
    (movq (% rsp) (% rbp))                  ;    [13]
    (pushq (% arg_y))                       ;    [16]
    (pushq (% arg_z))                       ;    [17]

;;; (+ a b)
    (movq (@ -8 (% rbp)) (% arg_y))         ;    [18]
    (movq (@ -16 (% rbp)) (% arg_z))        ;    [22]
    (movq (% rbp) (% rsp))                  ;    [26]
    (popq (% rbp))                          ;    [29]
    (movl (% arg_y.l) (% imm0.l))           ;    [30]
    (orl (% arg_z.l) (% imm0.l))            ;    [32]
    (testb ($ 7) (% imm0.b))                ;    [34]
    (jne L53)                               ;    [37]
    (addq (% arg_y) (% arg_z))              ;    [39]
    (jo L46)                                ;    [42]
    (repz)
    (retq)                                  ;    [44]
L46                                         ;   [@61]
    (jmp (@ .SPFIX-OVERFLOW))               ;    [46]

    (:align 2)
L53                                         ;   [@68]
    (jmp (@ .SPBUILTIN-PLUS))               ;    [53]

;;; #<no source text>

    (:align 4)
L65                                         ;   [@80]
    (uuo-error-wrong-number-of-args)        ;    [65]

And FOO2 to:

    (recover-fn-from-rip)                   ;     [0]
    (cmpl ($ 16) (% nargs))                 ;     [7]
    (jne L41)                               ;    [10]
    (pushq (% rbp))                         ;    [12]
    (movq (% rsp) (% rbp))                  ;    [13]
    (pushq (% arg_y))                       ;    [16]
    (pushq (% arg_z))                       ;    [17]

;;; (+ a b)
    (movq (@ -8 (% rbp)) (% arg_y))         ;    [18]
    (movq (@ -16 (% rbp)) (% arg_z))        ;    [22]
    (movq (% rbp) (% rsp))                  ;    [26]
    (popq (% rbp))                          ;    [29]
    (jmp (@ .SPBUILTIN-PLUS))               ;    [30]

;;; #<no source text>

    (:align 3)
L41                                         ;   [@56]
    (uuo-error-wrong-number-of-args)        ;    [41]

It feels like CCL has the same type information for FOO1 (using the global FTYPE declaration) and for FOO2 (using both the local TYPE declarations and the THE form for the return value). Yet the generated code is quite different.

What is CCL missing in FOO1 that leads to less compact generated code compared to FOO2? It seems to add an overflow check which is not present in FOO2.

Clozure / ccl

Global FTYPE declarations vs local TYPE declarations #459