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 455871c2..7c86c63a 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 @@ -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. diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt index 252a1ce9..1d434b32 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt +++ b/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))) + + ) ))