[racket] Puzzled about type inference

After some reflection, here is how I think you should proceed: 

#lang typed/racket

(: 1+ (Nonnegative-Integer -> Positive-Integer))
(define (1+ n)
  (+ n 1))

;; entirely unnecessary but helped me read 
(define-type (Maybe α) (U False α))
(define-type NI Nonnegative-Integer)
(define-type LNI (Listof NI))
(define-type VNI (Vectorof NI))
(define-type LVNI (Listof VNI))

(let* ((given  : LVNI '(#(1 2) #(3 4) #(5 6)))
       (length : NI   (1+ (apply max (map (lambda ({x : VNI}) (vector-ref x 0)) given))))
       (result : [Vectorof [Maybe NI]] (make-vector length #f)))
  (for ((q : VNI (in-list given)))
    (vector-set! result (vector-ref q 0) (vector-ref q 1)))
  result)


The above -- minus types -- is how I would probably write the code in Racket, following the style guide. (I would use three defines instead of let* but let's ignore this point.) I would use 
 -- given as a parameter (I am guessing here)
 -- length to tell the reader that this is the new length of the vector 
 -- result to spell out what this vector is about 

The for-loop would use a single line because it is short and brings across the idea. 

If I were to move this code to Typed Racket, I'd add a type declaration to each identifier just like in any other (explicitly, statically) typed programming language. That's what I did, and there was no problem checking and running your code. 

-- Matthias