Typecheck (lambda args body) as (arg1 -> result).

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

@@ -341,6 +341,12 @@
         [tc-e/t (lambda: ([x : Number] . [y : Boolean *]) (car y)) (->* (list N) B B)]
         [tc-e ((lambda: ([x : Number] . [y : Boolean *]) (car y)) 3) B]
         [tc-e (apply (lambda: ([x : Number] . [y : Boolean *]) (car y)) 3 '(#f)) B]
+        [tc-e (lambda args (void)) #:ret (ret (t:-> -String -Void) (-FS -top -bot))
+                                   #:expected (ret (t:-> -String -Void) (-FS -top -bot))]
+        [tc-e (lambda (x y . z) 
+                (+ x y (+ (length z))))
+              #:ret (ret (t:-> -Byte -Index N) (-FS -top -bot))
+              #:expected (ret (t:-> -Byte -Index N) (-FS -top -bot))]
 
         [tc-e/t (let: ([x : Number 3])
                       (when (number? x) #t))

collects/typed-racket/typecheck/tc-lambda-unit.rkt

@@ -72,7 +72,7 @@
                           [(> arg-len tys-len) (append arg-tys
                                                        (map (lambda _ (or rest-ty (Un)))
                                                             (drop arg-list tys-len)))]))])
-    (define (check-body)
+    (define (check-body [rest-ty rest-ty])
       (with-lexical-env/extend
        arg-list arg-types
        (make-lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null
@@ -80,7 +80,15 @@
                         ;; make up a fake name if none exists, this is an error case anyway
                         (and drest (cons (or rest (generate-temporary)) drest))
                         (tc-exprs/check (syntax->list body) ret-ty))))
-    (when (or (not (= arg-len tys-len))
+    ;; Check that the number of formal arguments is valid for the expected type.
+    ;; Thus it must be able to accept the number of arguments that the expected
+    ;; type has. So we check for three cases, if the function doesn't accept
+    ;; enough arguments, if it requires too many arguments, or if it doesn't
+    ;; support rest arguments if needed.
+    ;; This allows a form like (lambda args body) to have the type (-> Symbol
+    ;; Number) with out a rest arg.
+    (when (or (and (< arg-len tys-len) (not rest))
+              (> arg-len tys-len)
               (and (or rest-ty drest) (not rest)))
       (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest)))
     (cond
@@ -101,11 +109,10 @@
        (let ([rest-type (cond
                           [rest-ty rest-ty]
                           [(type-annotation rest) (get-type rest #:default Univ)]
-                          [(< arg-len tys-len) (list-ref arg-tys arg-len)]
+                          [else Univ])])
-                          [else (Un)])])
          (with-lexical-env/extend
           (list rest) (list (-lst rest-type))
-          (check-body)))])))
+          (check-body rest-type)))])))
 
 ;; typecheck a single lambda, with argument list and body
 ;; drest-ty and drest-bound are both false or not false
@@ -230,8 +237,10 @@
                                    #:when (and (not r) (not dr) (= (length a) (length (syntax->list fml)))))
                 f)]
              [else
+              ;; fml is an improper list, thus the function has a rest argument, and so valid
+              ;; types must have at least as many positional arguments as it does.
               (for/list ([a argss] [f fs]  [r rests] [dr drests]
-                                   #:when (and (or r dr) (= (length a) (sub1 (syntax-len fml)))))
+                                   #:when (>= (length a) (sub1 (syntax-len fml))))
                 f)])]
        [_ null]))
   (define (go expected formals bodies formals* bodies* nums-seen)