From b23016f86afbdd98a73fcb8f71d71a6ee5b8891c Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Tue, 11 Aug 2009 19:35:34 +0000
Subject: [PATCH] Prohibit predicates, unions of tvars in contracts Add vector?

svn: r15701
---
 collects/typed-scheme/private/base-env.ss      |  1 +
 collects/typed-scheme/private/type-contract.ss | 17 ++++++++++-------
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 55e0a68117..8c4e3f2ce4 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -183,6 +183,7 @@
 [- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))]
 [max (->* (list N) N N)]
 [min (->* (list N) N N)]
+[vector? (make-pred-ty (-vec Univ))]
 [vector-ref (-poly (a) ((-vec a) N . -> . a))]
 [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (-vec a)))]
 [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss
index ec0bb6b248..a1a2f784e6 100644
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@@ -4,7 +4,7 @@
 
 (require (except-in "../utils/utils.ss" extend))
 (require
- (rep type-rep)
+ (rep type-rep filter-rep object-rep)
  (typecheck internal-forms)
  (utils tc-utils require-contract)
  (env type-name-env)
@@ -64,19 +64,22 @@
         [(Base: sym cnt) cnt]
         [(Refinement: par p? cert)
          #`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
-        [(Union: elems) 
-         (with-syntax 
-             ([cnts (map t->c elems)])
-           #;(printf "~a~n" (syntax-object->datum #'cnts))
-           #'(or/c . cnts))]
+        [(Union: elems)         
+         (let-values ([(vars notvars)
+                       (partition F? elems)])
+           (unless (>= 1 (length vars)) (exit (fail)))
+           (with-syntax 
+               ([cnts (append (map t->c vars) (map t->c notvars))])
+             #'(or/c . cnts)))]
         [(Function: arrs)
          (let ()           
            (define (f a)
              (define-values (dom* rngs* rst)
                (match a
-                 [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
+                 [(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f '())
                   (values (map t->c/neg dom) (map t->c rngs) (and rst (t->c/neg rst)))]
                  [_ (exit (fail))]))
+             (trace f)
              (with-syntax 
                  ([(dom* ...) dom*]
                   [rng* (match rngs*