subtypep failure on or. cons types

[Paul F. Dietz]

This may or may not be new, but it's a small example so possibly useful for narrowing down the bug.

(subtypep '(cons sequence short-float)
          '(or (cons t (not cons))
               (cons function t)))

==> NIL, T

(when (subtypep '(cons sequence short-float) '(cons t (not cons))) ==> T, T)

[Christophe Rhodes (csr21-cantab)]

Thanks! I'm pretty sure this isn't new (it reproduces in sbcl 1.4.16
for me), but it's a nice illustration of the general problem: that when
we can't prove that some type is equivalent to another, its presence in
cons types makes us unduly sure of ourselves.

In this instance, the type algebra simplifies the union type
to include (CONS FUNCTION X) and (CONS (NOT FUNCTION) X), and then we
take intersections of those with (CONS SEQUENCE Y), and fail to
reconstruct the type SEQUENCE from the union

  (OR (AND FUNCTION SEQUENCE) (AND (NOT FUNCTION) SEQUENCE))

Also, thank you, this example has pointed me to what I think is a bug in
our handling of unions, which would also explain some of these broader
symptoms of too much certainty in subtype relationships. Specifically

  (let ((ctype1 (sb-kernel:specifier-type 'sequence))
        (ctype2 (sb-kernel:specifier-type
                 '(or (and function sequence) (and (not function) sequence)))))
    (sb-kernel:type= ctype1 ctype2))
  => NIL, T

This is a plain bug, untouched since I introduced it around 19 years
ago: our implementation of TYPE= on two union types does SUBTYPEP both
ways, and should return certainty only if _either_ subtype returns NIL,
T or _both_ return T, T. In this instance, the two SUBTYPEP results are
NIL, NIL and T, T -- but the current code incorrectly takes the
certainty value from T, T; this has knock-on consequences elsewhere.

Looking at the fallout from this now :) Thanks again!

[Christophe Rhodes (csr21-cantab)]

I've pushed a fix for type= on unions as 9c1032dd894f668e4ac9457a0dc5dde2eacceb37, which incidentally fixes ansi-tests SUBTYPEP.CONS.38 and SUBTYPEP.CONS.41. BUG040 from #1912863 still fails, and the SEQUENCE-in-disguise from the above comment is not recognized as SEQUENCE.

[Paul F. Dietz (paul-f-dietz)]

If you can surface whether a particular case has occurred in the internals (say, by setting some special variable to T when it happens) I can use random inputs to try to find an input that causes it. This would plug in cleanly to the subtypep tester I described in today's bug report, including pruning of the input.