Adds subtyping for filters, and fixes -FS to be more precise.

Closes PR 12817.

original commit: 0e0f1cd6707f5cda8e636f3dd1c6dd5d885fd0c4

collects/tests/typed-racket/unit-tests/subtype-tests.rkt

@@ -212,6 +212,17 @@
 
    [(-polydots (a) (->... (list) (a a) (make-ListDots a 'a)))
     (-polydots (b a) (->... (list b) (a a) (-pair b (make-ListDots a 'a))))]
+
+   [(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
+    (-> Univ -Boolean : (-FS -top -top))]
+   [(-> Univ -Boolean : (-FS -bot -bot))
+    (-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
+   [(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
+    (-> (Un -Symbol -String) -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
+   [FAIL
+    (-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
+    (-> Univ -Boolean : (-FS (-filter -String 0) (-not-filter -String 0)))]
+
    ))
 
 (define-go

collects/tests/typed-racket/unit-tests/typecheck-tests.rkt

@@ -373,7 +373,7 @@
 
         [tc-e (let ([x 1]) x) -One]
         [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS -bot -top))]
-        [tc-e (boolean? number?) #:ret (ret -Boolean (-FS -bot -top))]
+        [tc-e (boolean? number?) #:ret (ret -Boolean (-FS -bot (-not-filter B #'number?)))]
 
         [tc-e (let: ([x : (Option Number) #f]) x) (t:Un N (-val #f))]
         [tc-e (let: ([x : Any 12]) (not (not x))) -Boolean]
@@ -1102,7 +1102,7 @@
         ;(tc-e (false? #t) #:ret (ret B (-FS -bot -top)))
 
 
-        (tc-e (boolean? true) #:ret (ret B (-FS -top -bot)))
+        (tc-e (boolean? true) #:ret (ret B (-FS (-filter B #'true) -bot)))
         (tc-e (boolean? 6) #:ret (ret B (-FS -bot -top)))
         (tc-e (immutable? (cons 3 4)) B)
 
@@ -1271,11 +1271,13 @@
         (tc-e (namespace? (make-empty-namespace)) #:ret (ret B (-FS -top -bot)))
 
         (tc-e (namespace-anchor? 3) #:ret (ret B (-FS -bot -top)))
-        (tc-e/t (lambda: ((x : Namespace-Anchor)) (namespace-anchor? x)) (t:-> -Namespace-Anchor B : -true-lfilter))
+        (tc-e/t (lambda: ((x : Namespace-Anchor)) (namespace-anchor? x))
+                (t:-> -Namespace-Anchor B : (-FS (-filter -Namespace-Anchor 0) -bot)))
 
 
         (tc-e (variable-reference? 3) #:ret (ret B (-FS -bot -top)))
-        (tc-e/t (lambda: ((x : Variable-Reference)) (variable-reference? x)) (t:-> -Variable-Reference  B : -true-lfilter))
+        (tc-e/t (lambda: ((x : Variable-Reference)) (variable-reference? x))
+                (t:-> -Variable-Reference  B : (-FS (-filter -Variable-Reference 0) -bot)))
 
         (tc-e (system-type 'os) (one-of/c 'unix 'windows 'macosx))
         (tc-e (system-type 'gc) (one-of/c 'cgc '3m))
@@ -1625,6 +1627,9 @@
         [tc-e (filter values empty)
               (-lst -Bottom)]
 
+        [tc-e
+           ((inst filter Any Symbol) symbol? null)
+           (-lst -Symbol)]
         )
   (test-suite
    "check-type tests"

collects/typed-racket/types/base-abbrev.rkt

@@ -91,11 +91,8 @@
 
 
 (define/cond-contract (-FS + -)
-      (c:-> Filter/c Filter/c FilterSet?)
-      (match* (+ -)
-             [((Bot:) _) (make-FilterSet -bot -top)]
-             [(_ (Bot:)) (make-FilterSet -top -bot)]
-             [(+ -) (make-FilterSet + -)]))
+  (c:-> Filter/c Filter/c FilterSet?)
+  (make-FilterSet + -))
 
 (define/cond-contract (-filter t i [p null])
      (c:->* (Type/c name-ref/c) ((c:listof PathElem?)) Filter/c)

collects/typed-racket/types/subtype.rkt

@@ -154,6 +154,14 @@
       [(_ _)
        (fail! s t)])))
 
+;; check subtyping of filters, so that predicates subtype correctly
+(define (filter-subtype* A0 s t)
+  (match* (s t)
+   [(f f) A0]
+   [((Bot:) t) A0]
+   [(s (Top:)) A0]
+   [(_ _) (fail! s t)]))
+
 (define (subtypes/varargs args dom rst)
   (with-handlers
       ([exn:subtype? (lambda _ #f)])
@@ -514,12 +522,16 @@
               [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
               [((ValuesDots: s-rs s-dty dbound) (ValuesDots: t-rs t-dty dbound))
                (subtype* (subtypes* A0 s-rs t-rs) s-dty t-dty)]
-              ;; trivial case for Result
-              [((Result: t f o) (Result: t* f o))
-               (subtype* A0 t t*)]
-              ;; we can ignore interesting results
-              [((Result: t f o) (Result: t* (FilterSet: (Top:) (Top:)) (Empty:)))
-               (subtype* A0 t t*)]
+              [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) o))
+               (subtype-seq A0
+                 (subtype* t t*)
+                 (filter-subtype* ft ft*)
+                 (filter-subtype* ff ff*))]
+              [((Result: t (FilterSet: ft ff) o) (Result: t* (FilterSet: ft* ff*) (Empty:)))
+               (subtype-seq A0
+                 (subtype* t t*)
+                 (filter-subtype* ft ft*)
+                 (filter-subtype* ff ff*))]
               ;; subtyping on other stuff
               [((Syntax: t) (Syntax: t*))
                (subtype* A0 t t*)]