diff --git a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt index c3f68ac1..cde3c32a 100644 --- a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt +++ b/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 diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt index 73a9de5b..93227271 100644 --- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/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" diff --git a/collects/typed-racket/types/base-abbrev.rkt b/collects/typed-racket/types/base-abbrev.rkt index 28bd5fb2..5584fdaf 100644 --- a/collects/typed-racket/types/base-abbrev.rkt +++ b/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) diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index 774daabb..63428380 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/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*)]