From cece2ccc77f87bcd73d365906ec9260a8e1f3f08 Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Mon, 12 May 2014 23:03:09 -0700
Subject: [PATCH] Add support for tc-any-results having a filter.

original commit: 62c4f5d1fbb4f14d77a7e3c1b1020d53853060f4
---
 .../typed-racket/base-env/top-interaction.rkt |  2 +-
 .../typed-racket-lib/typed-racket/core.rkt    |  2 +-
 .../typed-racket/private/type-annotation.rkt  |  2 +-
 .../typed-racket/typecheck/check-below.rkt    | 50 ++++++++++++++-----
 .../typed-racket/typecheck/tc-app-helper.rkt  | 11 ++--
 .../typecheck/tc-app/tc-app-hetero.rkt        |  2 +-
 .../typecheck/tc-app/tc-app-list.rkt          |  2 +-
 .../typecheck/tc-app/tc-app-values.rkt        |  4 +-
 .../typed-racket/typecheck/tc-expr-unit.rkt   |  8 +--
 .../typed-racket/typecheck/tc-if.rkt          | 16 ++++--
 .../typecheck/tc-metafunctions.rkt            | 12 +++--
 .../typed-racket/typecheck/tc-subst.rkt       |  3 +-
 .../typed-racket/typecheck/tc-toplevel.rkt    | 10 ++--
 .../typed-racket/types/filter-ops.rkt         |  5 +-
 .../typed-racket/types/printer.rkt            |  2 +-
 .../typed-racket/types/tc-result.rkt          | 14 +++---
 .../unit-tests/check-below-tests.rkt          | 39 +++++++++------
 .../typed-racket/unit-tests/class-tests.rkt   |  2 +-
 .../unit-tests/typecheck-tests.rkt            | 20 ++++----
 19 files changed, 122 insertions(+), 84 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/top-interaction.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
index 2ef88f96..42585b34 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/top-interaction.rkt
@@ -86,7 +86,7 @@
                      (match type
                        [(tc-result1: t f o) t]
                        [(tc-results: t) (-values t)]
-                       [(tc-any-results:) ManyUniv]))))))]
+                       [(tc-any-results: f) (-AnyValues f)]))))))]
       [form
        (raise-syntax-error #f "must be applied to exactly one argument" #'form)]))
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/core.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/core.rkt
index f3888c42..4b71f629 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/core.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/core.rkt
@@ -74,7 +74,7 @@
                                [(tc-result1: (== -Void type-equal?))
                                 #f]
                                ;; don't print results of unknown type
-                               [(tc-any-results:)
+                               [(tc-any-results: f)
                                 #f]
                                [(tc-result1: t f o)
                                 ;; Don't display the whole types at the REPL. Some case-lambda types
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt
index 21b5bd07..5df50ebb 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt
@@ -81,7 +81,7 @@
            (tc-expr/check expr (ret anns))
            (let ([ty (tc-expr expr)])
              (match ty
-               [(tc-any-results:)
+               [(tc-any-results: _)
                 (tc-error/expr
                   "Expression should produce ~a values, but produces an unknown number of values"
                   (length stxs))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
index f4c865d2..006d3851 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
@@ -49,7 +49,7 @@
       ;; TODO simplify this case
       [(tc-results: ts _ _ dty _) (~a (length ts) " " (if (= (length ts) 1) "value" "values")
                                       " and `" dty " ...'")]
-      [(tc-any-results:) "unknown number"]))
+      [(tc-any-results: _) "unknown number"]))
   (type-mismatch
     (value-string expected) (value-string actual)
     "mismatch in number of values"))
@@ -91,18 +91,28 @@
 ;; Turns NoObject/NoFilter into the Empty/TopFilter
 (define (fix-results r)
   (match r
-    [(tc-any-results:) tc-any-results]
+    [(tc-any-results: f) (tc-any-results (fix-filter f -top))]
     [(tc-results: ts fs os)
      (ret ts (map fix-filter fs) (map fix-object os))]
     [(tc-results: ts fs os dty dbound)
      (ret ts (map fix-filter fs) (map fix-object os) dty dbound)]))
 
+(define (fix-results/bottom r)
+  (match r
+    [(tc-any-results: f) (tc-any-results (fix-filter f -bot))]
+    [(tc-results: ts fs os)
+     (ret ts (for/list ([f fs]) (fix-filter f -bot-filter)) (map fix-object os))]
+    [(tc-results: ts fs os dty dbound)
+     (ret ts (for/list ([f fs]) (fix-filter f -bot-filter)) (map fix-object os) dty dbound)]))
+
+
+
 ;; check-below : (/\ (Results Type -> Result)
 ;;                   (Results Results -> Result)
 ;;                   (Type Results -> Type)
 ;;                   (Type Type -> Type))
 (define (check-below tr1 expected)
-  (define (filter-better? f1 f2)
+  (define (filter-set-better? f1 f2)
     (match* (f1 f2)
       [(f f) #t]
       [(f (NoFilter:)) #t]
@@ -115,25 +125,42 @@
       [(o o) #t]
       [(o (or (NoObject:) (Empty:))) #t]
       [(_ _) #f]))
+  (define (filter-better? f1 f2)
+    (or (NoFilter? f2)
+        (implied-atomic? f2 f1)))
+
   (match* (tr1 expected)
-    ;; These two cases have to be first so that bottom (exceptions, etc.) can be allowed in cases
+    ;; This case has to be first so that bottom (exceptions, etc.) can be allowed in cases
     ;; where multiple values are expected.
     ;; We can ignore the filters and objects in the actual value because they would never be about a value
-    [((or (tc-any-results:) (tc-results: _) (tc-results: _ _ _ _ _)) (tc-any-results:)) tr1]
     [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
-     (fix-results expected)]
+     (fix-results/bottom expected)]
+
+    [((tc-any-results: f1) (tc-any-results: f2))
+     (unless (filter-better? f1 f2)
+       (type-mismatch f2 f1 "mismatch in filter"))
+     (tc-any-results (fix-filter f2 f1))]
+
+    [((or (tc-results: _ (list (FilterSet: fs+ fs-) ...) _)
+          (tc-results: _ (list (FilterSet: fs+ fs-) ...) _ _ _))
+      (tc-any-results: f2))
+     (define merged-filter (apply -and (map -or fs+ fs-)))
+     (unless (filter-better? merged-filter f2)
+       (type-mismatch f2 merged-filter "mismatch in filter"))
+     (tc-any-results (fix-filter f2 merged-filter))]
+
 
     [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
      (cond
        [(not (subtype t1 t2))
         (expected-but-got t2 t1)]
-       [(and (not (filter-better? f1 f2))
+       [(and (not (filter-set-better? f1 f2))
              (object-better? o1 o2))
         (type-mismatch f2 f1 "mismatch in filter")]
-       [(and (filter-better? f1 f2)
+       [(and (filter-set-better? f1 f2)
              (not (object-better? o1 o2)))
         (type-mismatch (print-object o2) (print-object o1) "mismatch in object")]
-       [(and (not (filter-better? f1 f2))
+       [(and (not (filter-set-better? f1 f2))
              (not (object-better? o1 o2)))
         (type-mismatch (format "`~a' and `~a'" f2 (print-object o2))
                        (format "`~a' and `~a'" f1 (print-object o1))
@@ -196,10 +223,7 @@
          (value-mismatch expected tr1))
      (fix-results expected)]
 
-    [((tc-any-results:) (tc-results: ts fs os))
-     (value-mismatch expected tr1)
-     (fix-results expected)]
-    [((tc-any-results:) (tc-results: ts fs os dty dbound))
+    [((tc-any-results: _) (? tc-results?))
      (value-mismatch expected tr1)
      (fix-results expected)]
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 447eaca3..9e728b23 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -6,7 +6,7 @@
          (contract-req)
          (typecheck check-below tc-subst)
          (utils tc-utils)
-         (rep type-rep)
+         (rep type-rep filter-rep)
          (except-in (types utils union abbrev subtype)
                     -> ->* one-of/c))
 (require-for-cond-contract
@@ -50,8 +50,7 @@
                           [ta (in-sequence-forever (in-list t-a) #f)])
                          (values oa ta))])
            (match rng
-            ;; TODO add filters to tc-any-results
-            [(AnyValues: f) tc-any-results]
+            [(AnyValues: f) (tc-any-results f)]
             [(Values: results)
              (define-values (t-r f-r o-r)
                (for/lists (t-r f-r o-r)
@@ -88,7 +87,7 @@
   (match t
     [(tc-result1: t) t]
     [(tc-results: ts) (-values ts)]
-    [(tc-any-results:) ManyUniv]
+    [(tc-any-results: f) (-AnyValues -top)]
     [_ t]))
 
 (define (stringify-domain dom rst drst [rng #f])
@@ -228,7 +227,7 @@
     (and expected
          (match expected
            [(tc-result1: t) t]
-           [(tc-any-results:) #t] ; anything is a subtype of expected
+           [(tc-any-results: (or (Top:) (NoFilter:))) #t] ; anything is a subtype of expected
            [_ #f]))) ; don't know what it is, don't do any pruning
   (define (returns-subtype-of-expected? fun-ty)
     (or (not expected) ; no expected type, anything is fine
@@ -249,7 +248,7 @@
     (map (compose make-Function list make-arr)
          doms
          (map (match-lambda ; strip filters
-               [(AnyValues: f) (-AnyValues f)]
+               [(AnyValues: f) (-AnyValues -top)]
                [(Values: (list (Result: t _ _) ...))
                 (-values t)]
                [(ValuesDots: (list (Result: t _ _) ...) _ _)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
index aea1941f..a047523f 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -133,7 +133,7 @@
          [(list t0) (tc/app/check #'(#%plain-app . form) (ret t0))]
          [_ (continue)])]
       ;; since vectors are mutable, if there is no expected type, we want to generalize the element type
-      [(or #f (tc-any-results:) (tc-result1: _))
+      [(or #f (tc-any-results: _) (tc-result1: _))
        (ret (make-HeterogeneousVector
               (for/list ((e (in-syntax #'(args ...))))
                 (generalize (tc-expr/t e)))))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
index 8ecf13fb..3651d0d2 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-list.rkt
@@ -40,7 +40,7 @@
        (unless (for/and ([b (in-list bound)]) (or (not b) (eq? bound0 b))) (fail))
        (define expected-elem-type
          (match expected
-           [(or #f (tc-any-results:)) #f]
+           [(or #f (tc-any-results: _)) #f]
            [(tc-result1: (ListDots: elem-type (== bound0))) (ret elem-type)]
            [(tc-result1: (Listof: elem-type)) (ret elem-type)]
            [else (fail)]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
index d42997f8..cde15892 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-values.rkt
@@ -22,13 +22,13 @@
     (match (tc/funapp #'prod #'() (single-value #'prod) null #f)
       [(tc-results: ts fs os)
        (tc/funapp #'con #'(prod) (single-value #'con) (map ret ts fs os) expected)]
-      [(tc-any-results:)
+      [(tc-any-results: _)
        (tc/app-regular this-syntax expected)]))
   ;; special case for `values' with single argument
   ;; we just ignore the values, except that it forces arg to return one value
   (pattern (values arg)
     (match expected
-     [(or #f (tc-any-results:)) (single-value #'arg)]
+     [(or #f (tc-any-results: _)) (single-value #'arg)]
      [(tc-result1: tp)
       (single-value #'arg expected)]
      [(tc-results: ts)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 97f642f4..c18817c7 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -160,7 +160,7 @@
       [(begin0 e . es)
        (begin0
          (tc-expr/check #'e expected)
-         (tc-body/check #'es tc-any-results))]
+         (tc-body/check #'es (tc-any-results -top)))]
       ;; if
       [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
       ;; lambda
@@ -185,7 +185,7 @@
                                   (Poly: _ (Function: _)))))
           (tc-expr/check/type #'fun (kw-convert f #:split #t))
           (ret f -true-filter)]
-         [(or (tc-results: _) (tc-any-results:))
+         [(or (tc-results: _) (tc-any-results: _))
           (tc-expr form)])]
       ;; opt function def
       [(~and (let-values ([(f) fun]) . body) opt:opt-lambda^)
@@ -361,10 +361,10 @@
 ;; The environment is extended with the propositions that are true if the expression returns
 ;; (e.g. instead of raising an error).
 (define (check-body-form e k)
-  (define results (tc-expr/check e tc-any-results))
+  (define results (tc-expr/check e (tc-any-results -no-filter)))
   (define props
     (match results
-      [(tc-any-results:) empty]
+      [(tc-any-results: f) (list f)]
       [(tc-results: _ (list (FilterSet: f+ f-) ...) _)
        (map -or f+ f-)]
       [(tc-results: _ (list (FilterSet: f+ f-) ...) _ _ _)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
index 89c1cccd..b1072715 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt
@@ -68,8 +68,14 @@
                [else
                 (add-neither tst)])
          (match* (results-t results-u)
-           [((tc-any-results:) _) tc-any-results]
-           [(_ (tc-any-results:)) tc-any-results]
+
+           [((tc-any-results: f1) (tc-any-results: f2))
+            (tc-any-results (-or (apply -and fs+ f1 new-thn-props) (apply -and fs- f2 new-els-props)))]
+           ;; Not do awful things here
+           [((tc-results: ts (list (FilterSet: f+ f-) ...) os) (tc-any-results: f2))
+            (tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
+           [((tc-any-results: f2) (tc-results: ts (list (FilterSet: f+ f-) ...) os))
+            (tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
            [((tc-results: ts fs2 os2)
              (tc-results: us fs3 os3))
             ;; if we have the same number of values in both cases
@@ -98,6 +104,6 @@
                   [(and (= 1 (length ts)) (type-equal? (car ts) (Un)))
                    (ret us fs3 os3)]
                   ;; otherwise, error
-               [else
-                (tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
-                               (length ts) (length us))])])))]))
+                  [else
+                   (tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
+                                  (length ts) (length us))])])))]))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
index f8e8a1c6..bc2c9c23 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
@@ -73,7 +73,7 @@
   (tc-results/c (listof identifier?) . -> . SomeValues/c)
   (define keys (for/list ([(nm k) (in-indexed arg-names)]) (list 0 k)))
   (match results
-    [(tc-any-results:) ManyUniv]
+    [(tc-any-results: f) (-AnyValues (abo arg-names keys f))]
     [(tc-results: ts fs os dty dbound)
      (make-ValuesDots
       (for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)])
@@ -167,7 +167,7 @@
 
 (define (tc-results->values tc)
   (match tc
-    [(tc-any-results:) ManyUniv]
+    [(tc-any-results: _) ManyUniv]
     [(tc-results: ts) (-values ts)]
     [(tc-results: ts _ _ dty dbound) (-values-dots ts dty dbound)]))
 
@@ -244,12 +244,14 @@
 ;; For each name replaces all uses of it in res with the corresponding object.
 ;; This is used so that names do not escape the scope of their definitions
 (define (replace-names names+objects res)
+  (define (sub proc i)
+    (for/fold ([s i]) ([name/object (in-list names+objects)])
+      (proc s (first name/object) (second name/object) #t)))
   (define (subber proc lst)
     (for/list ([i (in-list lst)])
-      (for/fold ([s i]) ([name/object (in-list names+objects)])
-        (proc s (first name/object) (second name/object) #t))))
+      (sub proc i)))
   (match res
-    [(tc-any-results:) res]
+    [(tc-any-results: f) (tc-any-results (sub subst-filter f))]
     [(tc-results: ts fs os)
      (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
     [(tc-results: ts fs os dt db)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index bf743184..e019618d 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -165,8 +165,7 @@
 (define/cond-contract (values->tc-results tc formals)
   (SomeValues/c (or/c #f (listof identifier?)) . -> . tc-results/c)
   (match tc
-    ;; TODO make tc-any-results have a filter
-    [(AnyValues: f) tc-any-results]
+    [(AnyValues: f) (tc-any-results f)]
     [(ValuesDots: (list (and rs (Result: ts fs os)) ...) dty dbound)
      (if formals
          (let-values ([(ts fs os)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
index 3ec3bde7..e2dbaf5c 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
@@ -179,7 +179,7 @@
 ;; typecheck the expressions of a module-top-level form
 ;; no side-effects
 ;; syntax? -> (or/c 'no-type tc-results/c)
-(define (tc-toplevel/pass2 form)
+(define (tc-toplevel/pass2 form [expected (tc-any-results -top)])
   
   (do-time (format "pass2 ~a line ~a"
                    (if #t
@@ -230,10 +230,12 @@
       [(begin) 'no-type]
       [(begin . rest)
        (for/last ([form (in-syntax #'rest)])
-         (tc-toplevel/pass2 form))]
+         (tc-toplevel/pass2 form expected))]
 
       ;; otherwise, the form was just an expression
-      [_ (tc-expr/check form tc-any-results)])))
+      [_ (if expected
+             (tc-expr/check form expected)
+             (tc-expr form))])))
 
 
 
@@ -424,6 +426,6 @@
        (register-parsed-struct-bindings! parsed))
      (tc-toplevel/pass1 form)
      (tc-toplevel/pass1.5 form)
-     (begin0 (tc-toplevel/pass2 form)
+     (begin0 (tc-toplevel/pass2 form #f)
              (report-all-errors))]))
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
index 2def959e..3c327f21 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
@@ -212,8 +212,7 @@
 ;; Useful to express properties of the form: if this expressions returns at all, we learn this
 (define (add-unconditional-prop results prop)
   (match results
-    ;; TODO add support for filters on tc-any-results
-    [(tc-any-results:) results]
+    [(tc-any-results: f) (tc-any-results (-and prop f))]
     [(tc-results: ts (list (FilterSet: fs+ fs-) ...) os)
      (ret ts
           (for/list ([f+ fs+] [f- fs-])
@@ -250,7 +249,7 @@
 ;; tc-results/c -> tc-results/c
 (define (erase-filter tc)
   (match tc
-    [(tc-any-results:) tc]
+    [(tc-any-results: _) (tc-any-results -no-filter)]
     [(tc-results: ts _ _)
      (ret ts
           (for/list ([f (in-list ts)]) -no-filter)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
index 18228d0a..64363491 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
@@ -480,7 +480,7 @@
     [(F: nm) nm]
     ;; FIXME (Values are not types and shouldn't need to be considered here
     [(AnyValues: (Top:)) 'AnyValues]
-    [(AnyValues: f) `(AnyValues : ,(filter->sexp f))]
+    [(AnyValues: f) (displayln (list 'this-case (NoFilter? f) (Top? f))) `(AnyValues : ,(filter->sexp f))]
     [(Values: (list v)) v]
     [(Values: (list v ...)) (cons 'values (map t->s v))]
     [(ValuesDots: v dty dbound)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
index 11ada36a..f096aed1 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
@@ -14,8 +14,7 @@
 (define-struct/cond-contract tc-results
   ([ts (c:listof tc-result?)] [drest (c:or/c (c:cons/c Type/c symbol?) #f)])
   #:transparent)
-(define-struct/cond-contract tc-any-results () #:transparent)
-(define tc-any-results* (tc-any-results))
+(define-struct/cond-contract tc-any-results ([f (c:or/c Filter/c NoFilter?)]) #:transparent)
 
 (define (tc-results/c v)
   (or (tc-results? v)
@@ -25,7 +24,7 @@
 ;; Used to contract the return values of typechecking functions.
 (define (full-tc-results/c r)
   (match r
-    [(tc-any-results:) #t]
+    [(tc-any-results: f) (not (equal? -no-filter f))]
     [(tc-results: _ fs os)
      (and
        (not (member -no-filter fs))
@@ -57,8 +56,8 @@
 
 (define-match-expander tc-any-results:
   (syntax-rules ()
-   [(_)
-    (tc-any-results)]))
+   [(_ f)
+    (tc-any-results f)]))
 
 
 (define-match-expander tc-result1:
@@ -150,11 +149,10 @@
 
 (define tc-result-equal? equal?)
 
-(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:
-         (rename-out
-           (tc-any-results* tc-any-results)))
+(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:)
 (provide/cond-contract
  [combine-results ((c:listof tc-results?) . c:-> . tc-results?)]
+ [tc-any-results ((c:or/c Filter/c NoFilter?) . c:-> . tc-any-results?)]
  [tc-result-t (tc-result? . c:-> . Type/c)]
  [rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
  [tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/check-below-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/check-below-tests.rkt
index 689ea87d..bec2dfc1 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/check-below-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/check-below-tests.rkt
@@ -31,7 +31,9 @@
     [(tc-results: ts fs os dty bound)
      (for-each check-filter fs)
      (for-each check-object os)]
-    [(or (tc-any-results:) (? Type/c?))
+    [(tc-any-results: f)
+     (check-filter f)]
+    [(? Type/c?)
      (void)]))
 
 
@@ -77,12 +79,12 @@
     (test-below
       (ret -Bottom)
       (ret (list Univ Univ) (list -true-filter -no-filter) (list -no-obj -empty-obj))
-      #:result (ret (list Univ Univ) (list -true-filter -top-filter) (list -empty-obj -empty-obj)))
+      #:result (ret (list Univ Univ) (list -true-filter -bot-filter) (list -empty-obj -empty-obj)))
 
     (test-below
       (ret -Bottom)
       (ret (list Univ) (list -no-filter) (list -no-obj) Univ 'B)
-      #:result (ret (list Univ) (list -top-filter) (list -empty-obj) Univ 'B))
+      #:result (ret (list Univ) (list -bot-filter) (list -empty-obj) Univ 'B))
 
     ;; Bottom is not below everything if the number of values doesn't match up.
     (test-below #:fail
@@ -117,17 +119,23 @@
       (ret (list -Symbol) (list -top-filter) (list -empty-obj))
       (ret (list Univ) (list -true-filter) (list (make-Path empty #'x))))
 
-    (test-below (ret -Bottom) tc-any-results #:result (ret -Bottom))
-    (test-below (ret Univ) tc-any-results #:result (ret Univ))
+    (test-below (ret -Bottom) (tc-any-results -no-filter) #:result (tc-any-results -bot))
+    (test-below (ret Univ) (tc-any-results -top) #:result (tc-any-results -top))
+    (test-below (tc-any-results -bot) (tc-any-results -no-filter) #:result (tc-any-results -bot))
+    (test-below
+      (ret (list -Symbol -String) (list -true-filter -bot-filter))
+      (tc-any-results -no-filter)
+      #:result (tc-any-results -bot))
+    (test-below (ret -Symbol -bot-filter) (tc-any-results -no-filter) #:result (tc-any-results -bot))
 
-    (test-below (ret -Symbol -true-filter -empty-obj) tc-any-results
-      #:result (ret -Symbol -true-filter -empty-obj))
-    (test-below (ret (list -Symbol -String)) tc-any-results
-      #:result (ret (list -Symbol -String)))
+    (test-below (ret -Symbol -true-filter -empty-obj) (tc-any-results -no-filter)
+      #:result (tc-any-results -top))
+    (test-below (ret (list -Symbol -String)) (tc-any-results -no-filter)
+      #:result (tc-any-results -top))
     (test-below
       (ret (list -Symbol -String) (list -true-filter -false-filter) (list -empty-obj -empty-obj))
-      tc-any-results
-      #:result (ret (list -Symbol -String) (list -true-filter -false-filter) (list -empty-obj -empty-obj)))
+      (tc-any-results -no-filter)
+      #:result (tc-any-results -top))
 
 
     (test-below #:fail
@@ -136,7 +144,7 @@
       #:result (ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj)))
 
     (test-below #:fail
-      tc-any-results
+      (tc-any-results -top)
       (ret -Symbol))
 
 
@@ -154,7 +162,7 @@
       #:result (ret -Symbol -top-filter -empty-obj Univ 'B))
 
     (test-below #:fail
-      tc-any-results
+      (tc-any-results -top)
       (ret -Symbol -no-filter -empty-obj Univ 'B)
       #:result (ret (list -Symbol) (list -top-filter) (list -empty-obj) Univ 'B))
 
@@ -162,8 +170,9 @@
       (ret -Symbol -top-filter -empty-obj Univ 'B)
       (ret (list -Symbol -Symbol) (list -top-filter -top-filter)  (list -empty-obj -empty-obj) Univ 'B))
 
-    (test-below (ret -Symbol -true-filter -empty-obj Univ 'B) tc-any-results
-                #:result (ret -Symbol -true-filter -empty-obj Univ 'B))
+    (test-below (ret -Symbol -true-filter -empty-obj Univ 'B)
+                (tc-any-results -no-filter)
+                #:result (tc-any-results -top))
 
     (test-below
       (ret -Symbol)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
index 61444893..4ac8828a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
@@ -107,7 +107,7 @@
          -Void]
    ;; Send to non object
    [tc-err (send 4 m 3)
-      #:ret (ret (-val 5))
+      #:ret (ret (-val 5) -bot-filter)
       #:expected (ret (-val 5) -no-filter -no-obj)]
    ;; Field access via get-field
    [tc-e (let ()
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 2fb16971..34634005 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -456,7 +456,7 @@
         [tc-e/t #(2 3 #t) (make-HeterogeneousVector (list -Integer -Integer -Boolean))]
         [tc-e (vector 2 "3" #t) (make-HeterogeneousVector (list -Integer -String -Boolean))]
         [tc-e (vector) (make-HeterogeneousVector (list))]
-        [tc-e (vector) (make-HeterogeneousVector (list)) #:expected tc-any-results]
+        [tc-e (vector) #:ret (tc-any-results -top) #:expected (tc-any-results -no-filter)]
         [tc-err (vector)
            #:ret (ret -Integer)
            #:expected (ret -Integer)]
@@ -893,7 +893,7 @@
         [tc-err (with-continuation-mark 1 2 (5 4))]
 
         [tc-err (with-continuation-mark 'x 'y 'z)
-          #:ret (ret (-val 'z))
+          #:ret (ret (-val 'z) -bot-filter)
           #:expected (ret (-val 'z) -no-filter -no-obj)]
 
 
@@ -1156,7 +1156,7 @@
         [tc-e/t (plambda: (a ...) ([x : Number] . [y : a ... a])
                           (andmap null? (map list y)))
                 (-polydots (a) ((list -Number) (a a) . ->... . -Boolean))]
-        [tc-e (ann (error 'foo) (values Number Number)) #:ret (ret (list -Number -Number))]
+        [tc-e (ann (error 'foo) (values Number Number)) #:ret (ret (list -Bottom -Bottom))]
 
         [tc-e (string->number "123")
               (t:Un (-val #f) -Number)]
@@ -2676,23 +2676,23 @@
          #:expected (ret (make-HeterogeneousVector (list -Byte -Byte)) -false-filter -no-obj)]
 
        [tc-err (values 'x)
-         #:ret (ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj))
+         #:ret (ret (list -Symbol -Symbol) (list -bot-filter -bot-filter) (list -empty-obj -empty-obj))
          #:expected (ret (list -Symbol -Symbol) (list -no-filter -no-filter ) (list -no-obj -no-obj))]
 
        [tc-err (values 'x 'y 'z)
-         #:ret (ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj))
+         #:ret (ret (list -Symbol -Symbol) (list -bot-filter -bot-filter) (list -empty-obj -empty-obj))
          #:expected (ret (list -Symbol -Symbol) (list -no-filter -no-filter ) (list -no-obj -no-obj))]
 
        [tc-err (values 'y)
-         #:ret (ret (list -Symbol) (list -top-filter ) (list -empty-obj) Univ 'B)
+         #:ret (ret (list -Symbol) (list -bot-filter ) (list -empty-obj) Univ 'B)
          #:expected (ret (list -Symbol) (list -no-filter ) (list -no-obj) Univ 'B)]
 
        [tc-err (values (values 'x 'y))
-         #:ret (ret (-val 'x))
+         #:ret (ret (-val 'x) -bot-filter)
          #:expected (ret (-val 'x) -no-filter -no-obj)]
 
        [tc-err (if (random) (values 1 2) 3)
-         #:ret (ret (-val 3) -top-filter)
+         #:ret (ret (-val 3) -true-filter)
          #:expected (ret (-val 3) -no-filter -no-obj)]
 
        [tc-err
@@ -2766,7 +2766,7 @@
                         (Number -> Number)))
            (define z (lambda (a) a))
            (z "y"))
-         #:ret (ret -String)
+         #:ret (ret -String -bot-filter)
          #:expected (ret -String -no-filter -no-obj)]
 
        [tc-err
@@ -2776,7 +2776,7 @@
                   (-> Symbol #:b Symbol Symbol)))
            (define z (lambda (a #:b b) a))
            (z "y" #:b "y"))
-         #:ret (ret -String)
+         #:ret (ret -String -bot-filter)
          #:expected (ret -String -no-filter -no-obj)]
 
        [tc-e/t