I think this should give a better error message already, because it calls `tc-expr` and then that's checked against the expected type later. Example:

````
Welcome to Racket v6.0.0.1.
-> (ann (lambda (x [z 0] #:y y . args) x) (values 1 2))
; readline-input:1:5: Type Checker: type mismatch;
;  mismatch in number of values
;   expected: 2
;   given: 1
;   in: (lambda (x (z 0) #:y y . args) x)
; [,bt for context]
; readline-input:1:5: Type Checker: type mismatch
;   expected: One 2
;   given: (case-> (Any #:y Any Any * -> Any) (Any Any #:y Any Any * -> Any))
;   in: (lambda (x (z 0) #:y y . args) x)
; [,bt for context]
; Type Checker: Summary: 2 errors encountered [,bt for context]
````