diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt index 5d7497d4..3c9469f5 100644 --- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/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)) diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt index d6c21d98..b1151b7b 100644 --- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/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 (Un)])]) + [else Univ])]) (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) @@ -241,7 +250,7 @@ (for/list ([f* formals*] [b* bodies*]) (match (find-expected expected f*) ;; very conservative -- only do anything interesting if we get exactly one thing that matches - [(list) + [(list) (if (and (= 1 (length formals*)) (match expected ((tc-results: _) #t) (_ #f))) (tc-error/expr #:return (list (lam-result null null (list #'here Univ) #f (ret (Un)))) "Expected a function of type ~a, but got a function with the wrong arity"