diff --git a/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl b/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl index eea91b7f1a..78e3cc495b 100644 --- a/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl +++ b/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 diff --git a/collects/tests/racket/benchmarks/shootout/typed/mandelbrot-generic.rktl b/collects/tests/racket/benchmarks/shootout/typed/mandelbrot-generic.rktl index 0edf7715d7..351cbae2e9 100644 --- a/collects/tests/racket/benchmarks/shootout/typed/mandelbrot-generic.rktl +++ b/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)) diff --git a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl index 3fce38ed9f..3ed28f8fc5 100644 --- a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl +++ b/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))) diff --git a/collects/tests/typed-scheme/succeed/generalize-vectors.rkt b/collects/tests/typed-scheme/succeed/generalize-vectors.rkt new file mode 100644 index 0000000000..7ac26bebde --- /dev/null +++ b/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) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt index 36f097a664..90f1d6e97c 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt +++ b/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)))] diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index 9613f06c49..b328aac73c 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/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 diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index cc65b03fb1..c5b185427c 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/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)))]