diff --git a/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl b/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl
index 78e3cc495b..eea91b7f1a 100644
--- a/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl
+++ b/collects/tests/racket/benchmarks/common/typed/nucleic3.rktl
@@ -278,6 +278,7 @@
 ;
 ; 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 351cbae2e9..0edf7715d7 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 (make-vector N 0.0)])
+  (let: ([v : (Vectorof Float) (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/meteor.rktl b/collects/tests/racket/benchmarks/shootout/typed/meteor.rktl
index 99ee462f09..75117b8730 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/meteor.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/meteor.rktl
@@ -91,7 +91,7 @@
 (define (no-islands? mask)
   (let ([zeros (zero-count mask)])
     (and (zeros . >= . 5)
-         (let loop ([mask mask] [zeros zeros])
+         (let: loop : Boolean ([mask : Integer mask] [zeros : Integer zeros])
            (if (= mask #x3FFFFFFFFFFFF)
              #t
              (let* ([p (assert (find-free-cell mask))]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/nbody-generic.rktl b/collects/tests/racket/benchmarks/shootout/typed/nbody-generic.rktl
index f00fd9504a..25287c5d0a 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/nbody-generic.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/nbody-generic.rktl
@@ -76,7 +76,8 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: offset-momentum ( -> Void))
 (define (offset-momentum)
-  (let loop-i ([i *system*] [px 0.0] [py 0.0] [pz 0.0])
+  (let: loop-i : Void ([i : (Listof body) *system*]
+                       [px : Float 0.0] [py : Float 0.0] [pz : Float 0.0])
     (if (null? i)
       (begin
         (set-body-vx! (car *system*) (/ (- px) +solar-mass+))
@@ -91,7 +92,7 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: energy ( -> Float))
 (define (energy)
-  (let loop-o ([o *system*] [e 0.0])
+  (let: loop-o : Float ([o : (Listof body) *system*] [e : Float 0.0])
     (if (null? o)
       e
       (let* ([o1 (car o)]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-generic.rktl b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-generic.rktl
index 86b604a7dc..2347175320 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-generic.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-generic.rktl
@@ -27,6 +27,7 @@ Correct output N = 1000 is
 
 (define +dt+ 0.01)
 
+(: make-body (Float * -> (Vectorof Float)))
 (define make-body vector)
 (define-syntax-rule (deffield n getter setter)
   (begin (define-syntax-rule (getter b) (vector-ref b n))
@@ -84,7 +85,8 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: offset-momentum ( -> Void))
 (define (offset-momentum)
-  (let loop-i ([i 0] [px 0.0] [py 0.0] [pz 0.0])
+  (let: loop-i : Void ([i : Natural 0]
+                       [px : Float 0.0] [py : Float 0.0] [pz : Float 0.0])
     (if (= i *system-size*)
       (begin
         (set-body-vx! (vector-ref *system* 0) (/ (- px) +solar-mass+))
@@ -99,7 +101,7 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: energy ( -> Float))
 (define (energy)
-  (let loop-o ([o 0] [e 0.0])
+  (let: loop-o : Float ([o : Natural 0] [e : Float 0.0])
     (if (= o *system-size*)
       e
       (let* ([o1 (vector-ref *system* o)]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-unsafe.rktl b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-unsafe.rktl
index a57e1ff568..c5679d68ff 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-unsafe.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec-unsafe.rktl
@@ -90,7 +90,8 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: offset-momentum ( -> Void))
 (define (offset-momentum)
-  (let loop-i ([i 0] [px 0.0] [py 0.0] [pz 0.0])
+  (let: loop-i : Void ([i : Natural 0]
+                       [px : Float 0.0] [py : Float 0.0] [pz : Float 0.0])
     (if (unsafe-fx= i *system-size*)
       (begin
         (set-body-vx! (unsafe-vector-ref *system* 0) (fl/ (fl- 0.0 px) +solar-mass+))
@@ -105,7 +106,7 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: energy ( -> Float))
 (define (energy)
-  (let loop-o ([o 0] [e 0.0])
+  (let: loop-o : Float ([o : Natural 0] [e : Float 0.0])
     (if (unsafe-fx= o *system-size*)
       e
       (let* ([o1 (unsafe-vector-ref *system* o)]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec.rktl b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec.rktl
index fe78b7b436..f133e32f3b 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/nbody-vec.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/nbody-vec.rktl
@@ -85,7 +85,8 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: offset-momentum ( -> Void))
 (define (offset-momentum)
-  (let loop-i ([i 0] [px 0.0] [py 0.0] [pz 0.0])
+  (let: loop-i : Void ([i : Natural 0]
+                       [px : Float 0.0] [py : Float 0.0] [pz : Float 0.0])
     (if (= i *system-size*)
       (begin
         (set-body-vx! (vector-ref *system* 0) (fl/ (fl- 0.0 px) +solar-mass+))
@@ -100,7 +101,7 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: energy ( -> Float))
 (define (energy)
-  (let loop-o ([o 0] [e 0.0])
+  (let: loop-o : Float ([o : Natural 0] [e : Float 0.0])
     (if (= o *system-size*)
       e
       (let* ([o1 (vector-ref *system* o)]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/nbody.rktl b/collects/tests/racket/benchmarks/shootout/typed/nbody.rktl
index 9828756499..12caa20d20 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/nbody.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/nbody.rktl
@@ -77,7 +77,8 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: offset-momentum ( -> Void))
 (define (offset-momentum)
-  (let loop-i ([i *system*] [px 0.0] [py 0.0] [pz 0.0])
+  (let: loop-i : Void ([i : (Listof body) *system*]
+                       [px : Float 0.0] [py : Float 0.0] [pz : Float 0.0])
     (if (null? i)
       (begin
         (set-body-vx! (car *system*) (fl/ (fl- 0.0 px) +solar-mass+))
@@ -92,7 +93,7 @@ Correct output N = 1000 is
 ;; -------------------------------
 (: energy ( -> Float))
 (define (energy)
-  (let loop-o ([o *system*] [e 0.0])
+  (let: loop-o : Float ([o : (Listof body) *system*] [e : Float 0.0])
     (if (null? o)
       e
       (let* ([o1 (car o)]
diff --git a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-generic.rktl
index 3ed28f8fc5..3fce38ed9f 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 (make-vector n 1.0)]
-        [v (make-vector n 0.0)])
+  (let: ([u : (Vectorof Float) (make-vector n 1.0)]
+         [v : (Vectorof Float) (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 (make-vector n 0.0)])
+  (let: ([u : (Vectorof Float) (make-vector n 0.0)])
     (MultiplyAv n v u)
     (MultiplyAtv n u AtAv)))
 
diff --git a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-unsafe.rktl b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-unsafe.rktl
index ec4bd015a6..61a990ccb9 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-unsafe.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm-unsafe.rktl
@@ -45,8 +45,8 @@
 (define (MultiplyAv n v Av)
   (for ([i (in-range n)])
     (flvector-set! Av i 
-                   (for/fold ([r 0.0])
-                       ([j (in-range n)])
+                   (for/fold: : Float ([r : Float 0.0])
+                       ([j : Natural (in-range n)])
                      (fl+ r (fl* (A i j) (flvector-ref v j)))))))
 
 ;; multiply vector v by matrix A transposed
@@ -54,8 +54,8 @@
 (define (MultiplyAtv n v Atv)
   (for ([i (in-range n)])
     (flvector-set! Atv i
-                   (for/fold ([r 0.0])
-                       ([j (in-range n)])
+                   (for/fold: : Float ([r : Float 0.0])
+                       ([j : Natural (in-range n)])
                      (fl+ r (fl* (A j i) (flvector-ref v j)))))))
 
 ;; multiply vector v by matrix A and then by matrix A transposed 
diff --git a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm.rktl b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm.rktl
index 6d936ffaac..24d9830743 100644
--- a/collects/tests/racket/benchmarks/shootout/typed/spectralnorm.rktl
+++ b/collects/tests/racket/benchmarks/shootout/typed/spectralnorm.rktl
@@ -18,7 +18,7 @@
     
     ;; B=AtA         A multiplied by A transposed
     ;; v.Bv /(v.v)   eigenvalue of v
-    (let loop ([i 0][vBv 0.0][vv 0.0])
+    (let: loop : Float ([i : Natural 0][vBv : Float 0.0][vv : Float 0.0])
       (if (= i n)
           (flsqrt (fl/ vBv vv))
           (let ([vi (flvector-ref v i)])
@@ -38,8 +38,8 @@
 (define (MultiplyAv n v Av)
   (for: : Void ([i : Natural (in-range n)])
     (flvector-set! Av i 
-                   (for/fold ([r 0.0])
-                       ([j (in-range n)])
+                   (for/fold: : Float ([r : Float 0.0])
+                       ([j : Natural (in-range n)])
                      (fl+ r (fl* (A i j) (flvector-ref v j)))))))
 
 ;; multiply vector v by matrix A transposed
@@ -47,8 +47,8 @@
 (define (MultiplyAtv n v Atv)
   (for: : Void ([i : Natural (in-range n)])
     (flvector-set! Atv i
-                   (for/fold ([r 0.0])
-                       ([j (in-range n)])
+                   (for/fold: : Float ([r : Float 0.0])
+                       ([j : Natural (in-range n)])
                      (fl+ r (fl* (A j i) (flvector-ref v j)))))))
 
 ;; multiply vector v by matrix A and then by matrix A transposed