From 59bdb6c9a86d9b4b471d49f4a0277279bb6c5985 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Sat, 25 Jan 2014 12:25:48 -0500
Subject: [PATCH] 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
---
 .../typed-racket/base-env/base-env.rkt        | 10 ++++++++--
 .../typed-racket/infer/infer-unit.rkt         | 20 ++++++++++++++++++-
 .../unit-tests/typecheck-tests.rkt            |  6 ++++++
 3 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 1a5c7f5f8b..cc80fabfcc 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/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))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 9d5d367d7b..b2302f0668 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/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))
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 265306d4bd..291491d9ab 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
@@ -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"