Generalization is now done on vector types.

collects/tests/racket/benchmarks/common/typed/nucleic3.rktl

@@ -278,7 +278,6 @@
 ;
 ; The components tx, ty, and tz are the translation vector.
 
-(: tfo-id (Vectorof Float))
 (define tfo-id  ; the identity transformation matrix
   '#(1.0 0.0 0.0
      0.0 1.0 0.0

collects/tests/racket/benchmarks/shootout/typed/mandelbrot-generic.rktl

@@ -12,7 +12,7 @@
 (define N.0 (exact->inexact N))
 (define 2/N (/ 2.0 N.0))
 (define Crs
-  (let: ([v : (Vectorof Float) (make-vector N 0.0)])
+  (let ([v (make-vector N 0.0)])
     (for ([x (in-range N)])
       (vector-set! v x (- (/ (* 2 x) N.0) 1.5)))
     v))

collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl

@@ -8,8 +8,8 @@
 
 (: Approximate (Natural -> Float))
 (define (Approximate n)
-  (let: ([u : (Vectorof Float) (make-vector n 1.0)]
-         [v : (Vectorof Float) (make-vector n 0.0)])
+  (let ([u (make-vector n 1.0)]
+        [v (make-vector n 0.0)])
     ;; 20 steps of the power method
     (for: : Void ([i : Natural (in-range 10)])
       (MultiplyAtAv n u v)
@@ -51,7 +51,7 @@
 ;; multiply vector v by matrix A and then by matrix A transposed 
 (: MultiplyAtAv (Natural (Vectorof Float) (Vectorof Float) -> Void))
 (define (MultiplyAtAv n v AtAv)
-  (let: ([u : (Vectorof Float) (make-vector n 0.0)])
+  (let ([u (make-vector n 0.0)])
     (MultiplyAv n v u)
     (MultiplyAtv n u AtAv)))
 

collects/tests/typed-scheme/succeed/generalize-vectors.rkt

@@ -0,0 +1,13 @@
+#lang typed/scheme
+
+(define x (vector 1.0 2.0)) ; should generalize to (Vectorof Float) even though it only contains Nonnegative-Floats
+(vector-set! x 0 -2.0)
+
+(define y (make-vector 2 1.0))
+(vector-set! y 0 -2.0)
+
+(define z #(1.0 2.0))
+(ann z (Vectorof Float))
+
+(define w (build-vector 3 (lambda: ((x : Integer)) (add1 x))))
+(vector-set! w 0 -2)

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -154,10 +154,10 @@
         [tc-e (void) -Void]
         [tc-e (void 3 4) -Void]
         [tc-e (void #t #f '(1 2 3)) -Void]
-        [tc-e/t #(3 4 5) (make-Vector -PositiveFixnum)]
+        [tc-e/t #(3 4 5) (make-Vector -Nat)]
         [tc-e/t '(2 3 4) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum)]
         [tc-e/t '(2 3 #t) (-lst* -PositiveFixnum -PositiveFixnum (-val #t))]
-        [tc-e/t #(2 3 #t) (make-Vector (t:Un -PositiveFixnum (-val #t)))]
+        [tc-e/t #(2 3 #t) (make-Vector (t:Un -Nat (-val #t)))]
         [tc-e/t '(#t #f) (-lst* (-val #t) (-val #f))]
         [tc-e/t (plambda: (a) ([l : (Listof a)]) (car l))
                 (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]

collects/typed-scheme/typecheck/tc-app.rkt

@@ -621,17 +621,51 @@
               (tc/funapp #'op #'(args ...) (single-value #'op) arg-tys expected))
             (check-below (for/first ([t ts]) (loop (ret t)))
                          expected))]
+	 ;; since vectors are mutable, if there is no expected type, we want to generalize the element type
          [(or #f (tc-result1: _))
-          (let ([arg-tys (map single-value (syntax->list #'(args ...)))])
+	  (let ([arg-tys (map (lambda (x)
+                              (match (single-value x)
+                                [(tc-result1: t) (ret (generalize t))]))
+                            (syntax->list #'(args ...)))])
             (tc/funapp #'op #'(args ...) (single-value #'op) arg-tys expected))]
          [_ (int-err "bad expected: ~a" expected)]))]
+    ;; since vectors are mutable, if there is no expected type, we want to generalize the element type
+    [(#%plain-app (~and op (~literal make-vector)) n elt)
+     (match expected
+       [(tc-result1: (Vector: t))
+        (tc-expr/check #'n (ret -Integer))
+        (tc-expr/check #'elt (ret t))
+        expected]
+       [(or #f (tc-result1: _))
+        (tc/funapp #'op #'(n elt) (single-value #'op)
+                   (list (single-value #'n)
+                         (match (single-value #'elt)
+                           [(tc-result1: t) (ret (generalize t))]))
+                   expected)]
+       [_ (int-err "bad expected: ~a" expected)])]
+    [(#%plain-app (~and op (~literal build-vector)) n proc)
+     (match expected
+       [(tc-result1: (Vector: t))
+        (tc-expr/check #'n (ret -Integer))
+        (tc-expr/check #'proc (ret (-NonnegativeFixnum . -> . t)))
+        expected]
+       [(or #f (tc-result1: _))
+        (tc/funapp #'op #'(n elt) (single-value #'op)
+                   (list (single-value #'n)
+                         (match (tc/funapp #'proc #'(1) ; valid nonnegative-fixnum
+                                           (single-value #'proc)
+                                           (list (ret -NonnegativeFixnum))
+                                           #f)
+                           [(tc-result1: t) (ret (-> -NonnegativeFixnum (generalize t)))]))
+                   expected)]
+       [_ (int-err "bad expected: ~a" expected)])]
     ;; special case for `-' used like `sub1'
     [(#%plain-app (~and op (~literal -)) v (~and arg2 ((~literal quote) 1)))
      (add-typeof-expr #'arg2 (ret -PositiveFixnum))
      (match-let ([(tc-result1: t) (single-value #'v)])
        (cond
-        [(subtype t -PositiveFixnum) (ret (Un -Zero -PositiveFixnum))]
-        [(subtype t (Un -Zero -PositiveFixnum)) (ret -Fixnum)]
+        [(subtype t -PositiveFixnum) (ret -NonnegativeFixnum)]
+        [(subtype t -NonnegativeFixnum) (ret -Fixnum)]
         [(subtype t -ExactPositiveInteger) (ret -Nat)]
         [else (tc/funapp #'op #'(v arg2) (single-value #'op) (list (ret t) (single-value #'arg2)) expected)]))]
     ;; call-with-values

collects/typed-scheme/typecheck/tc-expr-unit.rkt

@@ -82,7 +82,7 @@
        ;; errors are handled elsewhere
        [_ (make-Vector (apply Un 
                               (for/list ([l (syntax-e #'i)])
-                                (tc-literal l #f))))])]
+                                (generalize (tc-literal l #f)))))])]
     [(~var i (3d hash?))
      (let* ([h (syntax-e #'i)]
             [ks (hash-map h (lambda (x y) (tc-literal x)))]