Missing backpropagating type smartness

Consider the following two functions

(defun test-a (x)
  (flet ((bar (a)
           (* 4/3 a))
         (foo (a)
           (declare (type (integer -1 1) a))
           (+ 1 a)))
    (+ (bar x) (foo x))))

(defun test-b (x)
  (flet ((bar (a)
           (* 4/3 a))
         (foo (a)
           (declare (type (integer -1 1) a))
           (+ 1 a)))
    (+ (foo x) (bar x))))

They should always be equivalent for an exact value of X, and indeed, they give the same results. However, the type inference provides

CL-USER> (describe #'test-a)
#<FUNCTION TEST-A>
  [compiled function]

Lambda-list: (X)
Derived type: (FUNCTION (T) (VALUES NUMBER &OPTIONAL))

CL-USER> (describe #'test-b)
#<FUNCTION TEST-B>
  [compiled function]

Lambda-list: (X)
Derived type: (FUNCTION (T) (VALUES (RATIONAL -4/3 10/3) &OPTIONAL))

which are inequivalent (but not incorrect).

pkhuong suggests that the type checker constrains in the same direction as evaluation order, so since the second one provides constraints earlier in (FOO X), the constraints are propagated to (BAR X). However, when a general constraint is placed earlier on, it won't get constrained more.

It would be nice if the inferencer could backpropagate new constraints.

This was reproduced on Windows 7 x86-64 with SBCL 1.0.55 and Mac OS 10.8 on up to commit b75bc9ddf359ae9dcf25faf2f60f35aeb488e853.