ANSI-TEST SUBTYPEP.CONS.43 fails

[phoe]

The body of the failing test:

(deftest subtypep.cons.43
  (let* ((n -3.926510009989861d7)
         (t1 '(not (cons float t)))
         (t2 `(or (not (cons (eql 0) (real ,n ,n)))
                  (not (cons t (eql 0))))))
    (multiple-value-bind
     (sub1 good1)
     (subtypep* t1 t2)
     (multiple-value-bind
      (sub2 good2)
      (subtypep* `(not ,t2) `(not ,t1))
      (or (not good1)
          (not good2)
          (and sub1 sub2)
          (and (not sub1) (not sub2))))))
  t)

We are only interested in a part of this test. After simplifying:

(let* ((t1 '(not (cons float t)))
       (t2 `(or (not (cons (eql 0) (real -3.5d0 -3.5d0)))
                (not (cons t (eql 0))))))
  (subtypep t1 t2))

This evaluates to (VALUES NIL T), even though t2 is equivalent to T and therefore the valid results are (VALUES T T) and (VALUES NIL NIL).

[phoe]

Looks like the issue is in the type translator for NOT:

CL-USER> (funcall (ccl::info-type-translator 'not)
         `(NOT (OR (NOT CONS)
                   (CONS (INTEGER 0 0)
                         (OR (NOT INTEGER)
                             (INTEGER * -1)
                             (REAL (-3.926510009989861D+7))
                             (REAL * (-3.926510009989861D+7))))
                   (CONS (OR (NOT INTEGER)
                             (INTEGER * -1)
                             (INTEGER 1))
                         T)))
         (ccl::new-lexical-environment))
#<NAMED-CTYPE NIL>

[phoe]

Some more digging, following the logic in COERCE:

CCL> (defparameter *type* `(OR (NOT CONS)
                               (CONS (INTEGER 0 0)
                                     (OR (NOT INTEGER)
                                         (INTEGER * -1)
                                         (REAL (-3.926510009989861D+7))
                                         (REAL * (-3.926510009989861D+7))))
                               (CONS (OR (NOT INTEGER)
                                         (INTEGER * -1)
                                         (INTEGER 1))
                                     T)))
*TYPE*
CCL> (defparameter *ctype* (ccl::specifier-type *type*))
*CTYPE*
CCL> (union-ctype-types *ctype*)
(#<NEGATION-CTYPE (NOT CONS)> #<CONS-CTYPE (CONS (INTEGER 0 0) (OR (NOT INTEGER) (INTEGER * -1) (REAL (-3.926510009989861D+7)) (REAL * (-3.926510009989861D+7))))> #<CONS-CTYPE (CONS (OR (NOT INTEGER) (INTEGER * -1) (INTEGER 1)) T)>)
CCL> (second *)
#<CONS-CTYPE (CONS (INTEGER 0 0) (OR (NOT INTEGER) (INTEGER * -1) (REAL (-3.926510009989861D+7)) (REAL * (-3.926510009989861D+7))))>
CCL> (funcall #'(lambda (x) (specifier-type `(not ,(type-specifier x)))) *)
#<UNION-CTYPE (OR (NOT CONS) (CONS (OR (NOT INTEGER) (INTEGER * -1) (INTEGER 1)) T))>

In particular, we see that the negation of:

#<CONS-CTYPE
  (CONS (INTEGER 0 0)
        (OR (NOT INTEGER)
            (INTEGER * -1)
            (REAL (-3.926510009989861D+7))
            (REAL * (-3.926510009989861D+7))))>

is

#<UNION-CTYPE
  (OR (NOT CONS)
      (CONS (OR (NOT INTEGER)
                (INTEGER * -1)
                (INTEGER 1))
            T))>

E.g. the information about (REAL (-3.926510009989861D+7)) has been dropped from the second ctype, which smells of buggy behaviour to me.

[phoe]

EDIT: Sorry, I was wrong in this comment.

This type:

(OR (NOT INTEGER)
    (INTEGER * -1)
    (REAL (-3.926510009989861D+7))
    (REAL * (-3.926510009989861D+7)))

is actually T, since its negation is (AND INTEGER (NOT REAL)), which is NIL.

This means that the original type:

CCL> (defparameter *type* `(OR (NOT CONS)
                               (CONS (INTEGER 0 0)
                                     (OR (NOT INTEGER)
                                         (INTEGER * -1)
                                         (REAL (-3.926510009989861D+7))
                                         (REAL * (-3.926510009989861D+7))))
                               (CONS (OR (NOT INTEGER)
                                         (INTEGER * -1)
                                         (INTEGER 1))
                                     T)))

Is actually:

CCL> (defparameter *type* `(OR (NOT CONS)
                               (CONS (INTEGER 0 0)
                                     T)
                               (CONS (OR (NOT INTEGER)
                                         (INTEGER * -1)
                                         (INTEGER 1))
                                     T)))

Which in turn is actually:

CCL> (defparameter *type* `(OR (NOT CONS)
                               (CONS T T)))

Which is also T.

[phoe]

OK. We therefore need to go into the other branch of the test.

CCL is sure that

(NOT (CONS FLOAT T))

is NOT a subtype of

(OR (NOT (CONS (EQL 0) 
               (REAL -3.926510009989861D+7 -3.926510009989861D+7)))
    (NOT (CONS T (EQL 0))))

Even though the latter type is equivalent to T.

[phoe]

I've traced it down to:

(let* ((t1 '(not (cons float t)))
       (t2 `(or (not (cons (eql 0) (real #1=-3.5d0 #1#)))
                (not (cons t (eql 0)))))
       (c1 (ccl::specifier-type t1))
       (c2 (ccl::specifier-type t2)))
  (defparameter *type1* c1)
  (defparameter *type2* c2))

CCL> (union-simple-subtypep *type1* *type2*)
NIL
T

More digging required.

[phoe]

More digging: I have reduced the first type to (CONS (NOT FLOAT) T).

CCL> (csubtypep (specifier-type '(CONS (NOT FLOAT) T))
                (specifier-type `(OR (CONS (INTEGER 0 0)
                                           (OR (REAL * (-3.5D0))
                                               (NOT INTEGER)
                                               (INTEGER * -1)
                                               (REAL (-3.5D0))))
                                     (CONS (OR (NOT INTEGER)
                                               (INTEGER * -1)
                                               (INTEGER 1))
                                           T))))

[phoe]

I have dug my way all through CSUBTYPEP and have some more news.

CCL is sure that these two are not the same type, which is an error.

CCL> (type= (specifier-type
             `(OR (CONS (INTEGER 0 0)
                        (OR (REAL * (-3.5D0))
                            (NOT INTEGER)
                            (INTEGER * -1)
                            (REAL (-3.5D0))))
                  (CONS (OR (AND (NOT FLOAT) (NOT INTEGER))
                            (INTEGER * -1)
                            (INTEGER 1))
                        T)))
            (specifier-type
             `(CONS (NOT FLOAT) T)))
NIL
T

This is because of how the type method (union :complex-=) behaves:

(let ((type2 (specifier-type
              `(OR (CONS (INTEGER 0 0)
                         (OR (REAL * (-3.5D0))
                             (NOT INTEGER)
                             (INTEGER * -1)
                             (REAL (-3.5D0))))
                   (CONS (OR (AND (NOT FLOAT) (NOT INTEGER))
                             (INTEGER * -1)
                             (INTEGER 1))
                         T)))))
  (if (some #'type-might-contain-other-types-p
            (union-ctype-types type2))
      (values nil nil)
      (values nil t)))
NIL
T

So we check if any of the types of the union ctype might contain another type.

We do it like this:

(defun type-might-contain-other-types-p (type)
  (or (hairy-ctype-p type)
      (negation-ctype-p type)
      (union-ctype-p type)
      (intersection-ctype-p type)))

This list has no cons type, BUT, as we can see, the following type is a union type containing CONS types, and these CONS types add up to T:

(OR (CONS (INTEGER 0 0)
          (OR (REAL * (-3.5D0))
              (NOT INTEGER)
              (INTEGER * -1)
              (REAL (-3.5D0))))
    (CONS (OR (NOT INTEGER)
              (INTEGER * -1)
              (INTEGER 1))
          T))

Therefore we have a bug in our implementation - type-might-contain-other-types-p should also check for cons-ctype-p. Once we do that, the following happens:

CCL> (let* ((t1 '(not (cons float t)))
       (t2 `(or (not (cons (eql 0) (real #1=-3.5d0 #1#)))
                (not (cons t (eql 0)))))
       (c1 (ccl::specifier-type t1))
       (c2 (ccl::specifier-type t2)))
  (union-simple-subtypep c1 c2))
NIL
NIL

Which is not the best that we can do, but, at least, it is correct.

[phoe]

Fixed at phoe-trash@ba28152

[phoe]

Actually NOT fixed properly - the aforementioned commit might cause SUBTYPEP to behave more poorly and incorrectly return NIL NIL in some situations.

[phoe]

Hairy cons types are affected as well - @Bike found this on #lisp

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

[phoe]

Union types go out of the window, cons types are just as affected.

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

[Bike]

Here is what I believe is going on with the "go out the window" example. Since both types are cons types, the simple subtypep method is used, that is https://github.com/Clozure/ccl/blob/master/level-1/l1-typesys.lisp#L3333-L3341

This method computes the subtypep of the cars and the subtypep of the cdrs. It gets NIL NIL for the cars and T T for the second. So far so good. Then it merges these (on 3339-3341), and does so incorrectly: It decides that since it's certain that (satisfies foo2) is a subtype of t, it is certain that the first cons type is not a subtype of the second. Which is wrong.

The following truth table is ideal, I think, where T(ruth) = T T, F(alsity) = NIL T, and M(aybe) = NIL NIL:

 |TFM
-+---
T|TFM
F|FFF
M|MFM

whereas what's done now is

 |TFM
-+---
T|TFF
F|FFF
M|FFM

[Bike]

And I think the issue with the example I found is the same as the one with the range types, to be clear - the union type is all cons types, and those "never contain other types", so the complex-= method for unions erroneously concludes that the types are not equal.

[Bike]

I can't really think of a nice way to rewrite that erroneous if. the best i got is
(values (and val-car val-cdr) (or (and win-car win-cdr) (and (not val-car) win-car) (and (not val-cdr) win-cdr))), i.e. the second value is true if both of the subtypeps were certain or if at least one was certainly false.

[phoe]

@Bike I'll split the discussion of the SATISFIES issue into #252.

[phoe]

phoe-trash@d7fc6a