Make subtype work with restricted filters.

Closes PR 15025.

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

@@ -14,6 +14,7 @@
 (provide add-scope)
 
 (provide/cond-contract
+  [restrict-values (-> SomeValues/c (listof Type/c) SomeValues/c)]
   [values->tc-results (->* (SomeValues/c (listof Object?)) ((listof Type/c)) full-tc-results/c)]
   [replace-names (-> (listof (list/c identifier? Object?)) tc-results/c tc-results/c)])
 
@@ -32,6 +33,10 @@
                          [t (in-list ts)])
     (subst-tc-results res (list 0 arg) o #t t)))
 
+;; Restrict the objects in v refering to the current functions arguments to be of the types ts.
+(define (restrict-values v ts)
+  (for/fold ([v v]) ([t (in-list ts)] [arg (in-naturals)])
+    (subst-type v (list 0 arg) (-arg-path arg) #t t)))
 
 ;; replace-names: (listof (list/c identifier? Object?) tc-results? -> tc-results?
 ;; For each name replaces all uses of it in res with the corresponding object.

typed-racket-lib/typed-racket/types/subtype.rkt

@@ -10,7 +10,8 @@
 
 (lazy-require
   ("union.rkt" (Un))
-  ("../infer/infer.rkt" (infer)))
+  ("../infer/infer.rkt" (infer))
+  ("../typecheck/tc-subst.rkt" (restrict-values)))
 
 (define subtype-cache (make-hash))
 
@@ -103,19 +104,19 @@
         (arr: t1 t2 #f #f '()))
        (subtype-seq A0
                     (subtypes* t1 s1)
-                    (subtype* s2 t2))]
+                    (subtype* (restrict-values s2 t1) t2))]
       [((arr: s1 s2 #f #f s-kws)
         (arr: t1 t2 #f #f t-kws))
        (subtype-seq A0
                     (subtypes* t1 s1)
                     (kw-subtypes* s-kws t-kws)
-                    (subtype* s2 t2))]
+                    (subtype* (restrict-values s2 t1) t2))]
       [((arr: s-dom s-rng s-rest #f s-kws)
         (arr: t-dom t-rng #f #f t-kws))
        (subtype-seq A0
                     (subtypes*/varargs t-dom s-dom s-rest)
                     (kw-subtypes* s-kws t-kws)
-                    (subtype* s-rng t-rng))]
+                    (subtype* (restrict-values s-rng t-dom) t-rng))]
       [((arr: s-dom s-rng #f #f s-kws)
         (arr: t-dom t-rng t-rest #f t-kws))
        #f]
@@ -125,7 +126,7 @@
                     (subtypes*/varargs t-dom s-dom s-rest)
                     (subtype* t-rest s-rest)
                     (kw-subtypes* s-kws t-kws)
-                    (subtype* s-rng t-rng))]
+                    (subtype* (restrict-values s-rng t-dom) t-rng))]
       ;; handle ... varargs when the bounds are the same
       [((arr: s-dom s-rng #f (cons s-drest dbound) s-kws)
         (arr: t-dom t-rng #f (cons t-drest dbound) t-kws))
@@ -133,7 +134,7 @@
                     (subtype* t-drest s-drest)
                     (subtypes* t-dom s-dom)
                     (kw-subtypes* s-kws t-kws)
-                    (subtype* s-rng t-rng))]
+                    (subtype* (restrict-values s-rng t-dom) t-rng))]
       [(_ _) #f]))
 
 ;; check subtyping of filters, so that predicates subtype correctly

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

@@ -370,4 +370,9 @@
     (-prefab '(foo #(0)) -String)]
    [FAIL
     (-prefab '(foo #()) -String) (-prefab '(foo #(0)) (-opt -String))]
+
+   ;; Filter subtyping
+   ((make-pred-ty (list -Real) -Boolean (Un (-val 0.0) (-val 0)))
+    (make-pred-ty (list -Int) -Boolean (-val 0)))
+
    ))