Make the filter actually be opened up in the AnyValues case.

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt

@@ -18,7 +18,7 @@
 (define (open-Values v os ts)
   (match v
     [(AnyValues: f)
-     (tc-any-results f)]
+     (tc-any-results (open-Filter f os ts))]
     [(Values: results)
      (define-values (t-r f-r o-r)
        (for/lists (t-r f-r o-r)
@@ -33,6 +33,15 @@
      (ret t-r f-r o-r dty dbound)]))
 
 
+(define/cond-contract (open-Filter f objs ts)
+  (-> (Filter/c (listof Object?) (listof Type/c) Filter/c))
+  (for/fold ([f f])
+            ([(o arg) (in-indexed (in-list objs))]
+             [arg-ty (in-list ts)])
+    (define key (list 0 arg))
+    (subst-filter f key o #t)))
+
+
 ;; Substitutes the given objects into the type, filters, and object
 ;; of a Result for function application. This matches up to the substitutions
 ;; in the T-App rule from the ICFP paper.

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt

@@ -132,5 +132,12 @@
                      (list (make-Path null #'x)) (list Univ))
         (ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol #'x) -top)))))
 
+      ;; Substitute into filter of any values
+      (check-equal?
+        (open-Values (make-AnyValues (-filter -String '(0 0)))
+                     (list (make-Path null #'x)) (list Univ))
+        (tc-any-results (-filter -String #'x)))
+
+
     )
   ))