Prohibit predicates, unions of tvars in contracts

Add vector?

svn: r15701

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)))]

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)
@@ -65,18 +65,21 @@
         [(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))]
+         (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*