From d30ba6ac02b0f8edb5c892be80a97cddcc2213a2 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Mon, 17 May 2010 18:03:34 -0400
Subject: [PATCH] More fixes for Vincent.

original commit: 535dc73fad6d22a5a057d18aa0ba4ff00f926810
---
 .../typed-scheme/fail/subtype-int-err.rkt     | 22 ++++++++++++++
 .../typed-scheme/succeed/poly-ret-ann.rkt     |  6 ++++
 .../typed-scheme/typecheck/tc-lambda-unit.rkt |  3 +-
 collects/typed-scheme/typecheck/tc-subst.rkt  | 30 +++++++++++--------
 4 files changed, 48 insertions(+), 13 deletions(-)
 create mode 100644 collects/tests/typed-scheme/fail/subtype-int-err.rkt
 create mode 100644 collects/tests/typed-scheme/succeed/poly-ret-ann.rkt

diff --git a/collects/tests/typed-scheme/fail/subtype-int-err.rkt b/collects/tests/typed-scheme/fail/subtype-int-err.rkt
new file mode 100644
index 00000000..c58b8226
--- /dev/null
+++ b/collects/tests/typed-scheme/fail/subtype-int-err.rkt
@@ -0,0 +1,22 @@
+#;
+(exn-pred 2)
+#lang typed/scheme/base
+
+(: gen-lambda-n-rest ((Any -> Any)
+                     -> (Any -> (Any Any Any Any * -> Any))))
+(define (gen-lambda-n-rest body)
+ (error 'fail))
+
+(: gen-lambda (Integer Any -> (Any -> (Any * -> Any))))
+(define (gen-lambda nb-vars body)
+ (case nb-vars
+   ((3)  (gen-lambda-3 body))
+   (else (gen-lambda-n nb-vars body))))
+
+(: gen-lambda-3 (Any -> (Any -> (Any Any Any -> Any))))
+(define (gen-lambda-3 body)
+ (error 'fail))
+
+(: gen-lambda-n (Integer Any -> (Any -> (Any Any Any Any * -> Any))))
+(define (gen-lambda-n nb-vars body)
+ (error 'fail))
\ No newline at end of file
diff --git a/collects/tests/typed-scheme/succeed/poly-ret-ann.rkt b/collects/tests/typed-scheme/succeed/poly-ret-ann.rkt
new file mode 100644
index 00000000..c8e0c901
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/poly-ret-ann.rkt
@@ -0,0 +1,6 @@
+
+#lang typed/scheme/base
+(: f (Integer -> (All (X) (X -> X))))
+(define (f x)
+ (add1 x)
+ (lambda (x) x))
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
index c76ba74c..4aab25a9 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt
@@ -244,7 +244,8 @@
       [(tc-result1: (or (Poly: _ _) (PolyDots: _ _)))
        (tc/plambda form formals bodies expected)]
       [(tc-result1: (Error:)) (tc/mono-lambda/type formals bodies #f)]
-      [_ (int-err "expected not an appropriate tc-result: ~a" expected)]))
+      [(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))]
+      [(tc-result1: t) (int-err "expected not an appropriate tc-result: ~a ~a" expected t)]))
   (match expected
     [(tc-result1: (and t (Poly-names: ns expected*)))
      (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
diff --git a/collects/typed-scheme/typecheck/tc-subst.rkt b/collects/typed-scheme/typecheck/tc-subst.rkt
index 4377abee..7f07fa6b 100644
--- a/collects/typed-scheme/typecheck/tc-subst.rkt
+++ b/collects/typed-scheme/typecheck/tc-subst.rkt
@@ -143,18 +143,24 @@
    (for-type type)
     #f))
 
+
+
 ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
 (d/c (values->tc-results tc formals)
-  ((or/c Values? ValuesDots?) (listof identifier?) . -> . tc-results?)
+  ((or/c Values? ValuesDots?) (or/c #f (listof identifier?)) . -> . tc-results?)
   (match tc
-    [(ValuesDots: (list rs ...) dty dbound)
-     (let-values ([(ts fs os) 
-                   (for/lists (ts fs os) ([r (in-list rs)]) 
-                              (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
-       (ret ts fs os
-            (for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
-              (subst-type dty k (make-Path null o) #t))
-            dbound))]
-    [(Values: (list rs ...))
-     (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
-       (ret ts fs os))]))
+    [(ValuesDots: (list (and rs (Result: ts fs os)) ...) dty dbound)
+     (if formals
+         (let-values ([(ts fs os) 
+                       (for/lists (ts fs os) ([r (in-list rs)]) 
+                         (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+           (ret ts fs os
+                (for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
+                  (subst-type dty k (make-Path null o) #t))
+                dbound))
+         (ret ts fs os dty dbound))]
+    [(Values: (list (and rs (Result: ts fs os)) ...))
+     (if formals
+         (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+           (ret ts fs os))
+         (ret ts fs os))]))