Improve type inference for ValuesDots types

Add more precise types for `call-with-input-string`
that take advantage of the improved inference.

Closes PR 14050

original commit: 59bdb6c9a86d9b4b471d49f4a0277279bb6c5985

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt

@@ -1605,8 +1605,14 @@
 [with-output-to-bytes
   (-> (-> ManyUniv) -Bytes)]
 
-[call-with-input-string (-poly (a) (-> -String (-> -Input-Port a) a))]
-[call-with-input-bytes (-poly (a) (-> -Bytes (-> -Input-Port a) a))]
+[call-with-input-string
+ (-polydots (a)
+   (-> -String (-> -Input-Port (make-ValuesDots '() a 'a))
+       (make-ValuesDots '() a 'a)))]
+[call-with-input-bytes
+ (-polydots (a)
+   (-> -Bytes (-> -Input-Port (make-ValuesDots '() a 'a))
+       (make-ValuesDots '() a 'a)))]
 
 [with-input-from-string (-poly (a) (-> -String (-> a) a))]
 [with-input-from-bytes (-poly (a) (-> -Bytes (-> a) a))]

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -386,12 +386,30 @@
            (let* ([vars     (var-store-take dbound s-dty (- (length ts) (length ss)))]
                   ;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
                   [new-tys  (for/list ([var (in-list vars)])
-                              (substitute (make-F var) dbound s-dty))]
+                              ;; must be a Result since we are matching these against
+                              ;; the contents of the `Values`, which are Results
+                              (make-Result
+                               (substitute (make-F var) dbound s-dty)
+                               -no-filter -no-obj))]
                   ;; generate constraints on the prefixes, and on the dummy types
                   [new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
              ;; now take all the dummy types, and use them to constrain dbound appropriately
              (move-vars-to-dmap new-cset dbound vars))]
 
+          ;; like the case above, but constrains `dbound' to be |ss| - |ts|
+          [((Values: ss) (ValuesDots: ts t-dty dbound))
+           (unless (>= (length ss) (length ts)) (fail! ss ts))
+           (unless (memq dbound Y) (fail! S T))
+
+           ;; see comments for last case, this case swaps `s` and `t` order
+           (let* ([vars     (var-store-take dbound t-dty (- (length ss) (length ts)))]
+                  [new-tys  (for/list ([var (in-list vars)])
+                              (make-Result
+                               (substitute (make-F var) dbound t-dty)
+                               -no-filter -no-obj))]
+                  [new-cset (cgen/list V (append vars X) Y ss (append ts new-tys))])
+             (move-vars-to-dmap new-cset dbound vars))]
+
           ;; identical bounds - just unify pairwise
           [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
            (when (memq dbound Y) (fail! ss ts))

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

@@ -152,6 +152,7 @@
   racket/list
   racket/math
   racket/path
+  racket/port
   racket/sequence
   racket/set
   racket/string
@@ -1942,6 +1943,11 @@
              #:ret (ret (-HT -Symbol -String)
                         (-FS -top -top)
                         (make-NoObject))]
+       ;; call-with-input-string and friends - PR 14050
+       [tc-e (call-with-input-string "abcd" (lambda: ([input : Input-Port]) (values 'a 'b)))
+             #:ret (ret (list (-val 'a) (-val 'b)))]
+       [tc-e (call-with-input-bytes #"abcd" (lambda: ([input : Input-Port]) (values 'a 'b)))
+             #:ret (ret (list (-val 'a) (-val 'b)))]
         )
   (test-suite
    "tc-literal tests"