SUBTYPEP with CONS SATISFIES is overconfident

[phoe]

(defun foo (x) (declare (ignore x)) (= 1 (random 2)))
(defun foo2 (x) (declare (ignore x)) (= 1 (random 2)))
(defun bar (x) (declare (ignore x)) (= 1 (random 2)))
(defun bar2 (x) (declare (ignore x)) (= 1 (random 2)))

CCL> (subtypep `(or (cons (satisfies foo)
                          (satisfies foo2))
                    (cons (satisfies bar)
                          (satisfies bar2))) 
               `(cons (not float)))
NIL
T

CCL> (subtypep `(cons (satisfies foo) (satisfies foo2)) 
               `(cons (not float) t))
NIL
T

@Bike has some comments on the matter: https://github.com/Clozure/ccl/issues/249#issuecomment-555180049 https://github.com/Clozure/ccl/issues/249#issuecomment-555181115 https://github.com/Clozure/ccl/issues/249#issuecomment-555191047

[phoe]

Defining the predicates:

(defun foo (x) (declare (ignore x)) (= 1 (random 2)))
(defun foo2 (x) (declare (ignore x)) (= 1 (random 2)))
(defun bar (x) (declare (ignore x)) (= 1 (random 2)))
(defun bar2 (x) (declare (ignore x)) (= 1 (random 2)))

@Bike with the fix, we get:

CL-USER> (subtypep `(or (cons (satisfies foo)
                              (satisfies foo2))
                        (cons (satisfies bar)
                              (satisfies bar2))) 
                   `(cons (not float)))
NIL
NIL

But the contraposition does not hold:

CL-USER> (subtypep `(not (cons (not float)))
                   `(not (or (cons (satisfies foo)
                                   (satisfies foo2))
                             (cons (satisfies bar)
                                   (satisfies bar2)))))
NIL
T

[Bike]

Seems like a different issue to me, or rather the previous issue. Both of those end up as union ctypes so it goes through the same type= thing you explained before.