From a522768b7e847da2be73c66523da95e4218873ab Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Tue, 7 Apr 2015 09:39:46 -0700
Subject: [PATCH] Make tc-subst restrict returned types based on argument
 types.

---
 .../typed-racket/typecheck/tc-subst.rkt       | 25 ++++++++++++++++---
 typed-racket-test/optimizer/tests/list.rkt    |  2 +-
 .../unit-tests/metafunction-tests.rkt         |  4 +--
 .../unit-tests/typecheck-tests.rkt            | 13 ++++++----
 4 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
index 0477508e..fc9d9d91 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
@@ -53,17 +53,34 @@
 (define/cond-contract (subst-tc-results res k o polarity t)
   (-> full-tc-results/c name-ref/c Object? boolean? Type? full-tc-results/c)
   (define (st ty) (subst-type ty k o polarity t))
+  (define (sr ty fs ob) (subst-tc-result ty fs ob k o polarity t))
   (define (sf f) (subst-filter f k o polarity t))
-  (define (sfs fs) (subst-filter-set fs k o polarity t))
-  (define (so ob) (subst-object ob k o polarity))
   (match res
     [(tc-any-results: f) (tc-any-results (sf f))]
     [(tc-results: ts fs os)
-     (ret (map st ts) (map sfs fs) (map so os))]
+     (tc-results (map sr ts fs os) #f)]
     [(tc-results: ts fs os dt db)
-     (ret (map st ts) (map sfs fs) (map so os) (st dt) db)]))
+     (tc-results (map sr ts fs os) (cons (st dt) db))]))
 
 
+;; Substitution of objects into a tc-result
+;; This is a combination of the other substitutions, plus a restriction of the returned type
+;; to the arguments type if the returned object corresponds to an argument.
+(define (subst-tc-result r-t r-fs r-o k o polarity t)
+  (define argument-side
+    (match r-o
+      [(Path: p (? (lambda (nm) (name-ref=? nm k))))
+       (path-type p t)]
+      [_ Err]))
+
+  (tc-result
+    (if (equal? argument-side Err)
+        (subst-type r-t k o polarity t)
+        (restrict argument-side
+                  (subst-type r-t k o polarity t)))
+    (subst-filter-set r-fs k o polarity t)
+    (subst-object r-o k o polarity)))
+
 ;; Substitution of objects into a filter set
 ;; This is essentially ψ+|ψ- [o/x] from the paper
 (define/cond-contract (subst-filter-set fs k o polarity t)
diff --git a/typed-racket-test/optimizer/tests/list.rkt b/typed-racket-test/optimizer/tests/list.rkt
index f836f5e4..e54ddb1e 100644
--- a/typed-racket-test/optimizer/tests/list.rkt
+++ b/typed-racket-test/optimizer/tests/list.rkt
@@ -1,10 +1,10 @@
 #;#;
 #<<END
-TR missed opt: list.rkt 6:0 (rest (rest l)) -- car/cdr on a potentially empty list -- caused by: 6:6 (rest l)
 TR opt: list.rkt 3:0 (first l) -- pair
 TR opt: list.rkt 4:0 (rest l) -- pair
 TR opt: list.rkt 5:0 (second l) -- pair
 TR opt: list.rkt 5:0 (second l) -- pair
+TR opt: list.rkt 6:0 (rest (rest l)) -- pair
 TR opt: list.rkt 6:6 (rest l) -- pair
 TR opt: list.rkt 7:0 (third l) -- pair
 TR opt: list.rkt 7:0 (third l) -- pair
diff --git a/typed-racket-test/unit-tests/metafunction-tests.rkt b/typed-racket-test/unit-tests/metafunction-tests.rkt
index cf02e5a4..7228cd21 100644
--- a/typed-racket-test/unit-tests/metafunction-tests.rkt
+++ b/typed-racket-test/unit-tests/metafunction-tests.rkt
@@ -118,10 +118,10 @@
 
       ;; Check additional filters
       (check-equal?
-        (values->tc-results (make-Values (list (-result (-opt -Symbol) (-FS (-not-filter -String '(0 0)) -top)
+        (values->tc-results (make-Values (list (-result (-opt -String) (-FS -top (-not-filter -String '(0 0)))
                                                  (make-Path null '(0 0)))))
                             (list (make-Path null #'x)) (list -String))
-        (ret (-opt -Symbol) -false-filter (make-Path null #'x)))
+        (ret -String -true-filter (make-Path null #'x)))
 
       ;; Substitute into ranges correctly
       (check-equal?
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index b6798a8e..f349ef8e 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -672,7 +672,7 @@
         [tc-e ((inst add-between Positive-Byte Symbol) '(1 2 3) 'a #:splice? #t #:before-first '(b))
               (-lst (t:Un -PosByte -Symbol))]
 
-        [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -PosByte)]
+        [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (unfold (-lst -PosByte))]
         [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -PosByte)]
 
         [tc-err ((case-lambda: [([x : Number]) x]
@@ -2686,7 +2686,7 @@
                (string-append x y))
              -String]
        [tc-e (let loop ([x "x"]) x)
-             #:ret (ret Univ -true-filter)]
+             #:ret (ret -String -true-filter)]
        [tc-e (let loop ([x : String "x"]) x)
              #:ret (ret -String -true-filter)]
        [tc-e (let/cc k "foo") -String]
@@ -3023,7 +3023,7 @@
        [tc-err
          (let ([f (lambda (x y) y)])
            (f 1 2 3))
-         #:ret (ret Univ -true-filter)]
+         #:ret (ret -PosByte -true-filter)]
 
        [tc-err
          (case-lambda
@@ -3328,7 +3328,7 @@
 
        [tc-e
          ((if (even? 4) add1 (inst values Integer)) 4)
-         -Int]
+         -PosIndex]
 
        ;; PR 14601
        [tc-err
@@ -3609,7 +3609,7 @@
        [tc-e/t (lambda: ([x : One])
                  (let ([f (lambda: [w : Any *] w)])
                    (f x "hello" #\c)))
-        (t:-> -One (-lst Univ) : -true-filter)]
+        (t:-> -One (unfold (-lst Univ)) : -true-filter)]
 
        [tc-e/t (lambda: ([x : One])
                  (let ([f (plambda: (a ...) [w : a ... a] w)])
@@ -3628,6 +3628,9 @@
        [tc-e/t
          (lambda: ([x : Byte]) (if (< 0 x) x 1))
          (t:-> -Byte -PosByte : (-FS (-filter -Byte (list 0 0)) -bot))]
+
+       [tc-e/t ((inst values Any) "a") -String]
+       [tc-e ((inst second Any Any Any) (list "a" "b")) -String]
        )
 
   (test-suite