diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/annotate-classes.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/annotate-classes.rkt index a3e1aa2f..5b780640 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/annotate-classes.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/annotate-classes.rkt @@ -147,3 +147,15 @@ (define-splicing-syntax-class optional-standalone-annotation (pattern (~optional a:standalone-annotation) #:with ty (if (attribute a) #'a.ty #f))) + +(define-splicing-syntax-class lambda-type-vars + #:description "optional type parameters" + #:attributes (type-vars) + (pattern (~seq (~or #:forall #:∀) (var:id ...)) + #:attr type-vars #'(var ...))) + +(define-splicing-syntax-class maybe-lambda-type-vars + #:description "optional type parameters" + #:attributes (type-vars) + (pattern :lambda-type-vars) + (pattern (~seq) #:attr type-vars #f)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt index d10afc2b..fcec9a53 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -496,6 +496,15 @@ This file defines two sorts of primitives. All of them are provided into any mod (lambda (bs.ann-name ...) . #,(syntax/loc stx body)))]) #,(quasisyntax/loc stx nm)))]) bs.rhs ...))] + [(-let ([bn:optionally-annotated-name e] ...) + vars:lambda-type-vars . rest) + (define/with-syntax (bn* ...) + ;; singleton names go to just the name + (for/list ([bn (in-syntax #'(bn ...))]) + (if (empty? (stx-cdr bn)) + (stx-car bn) + bn))) + (template ((-lambda (bn* ...) (?@ . vars) . rest) e ...))] [(-let . rest) (syntax/loc stx (-let-internal . rest))])) @@ -1229,7 +1238,9 @@ This file defines two sorts of primitives. All of them are provided into any mod (define-syntax (-lambda stx) (syntax-parse stx #:literals (:) - [(_ formals:lambda-formals return:return-ann + [(_ formals:lambda-formals + vars:maybe-lambda-type-vars + return:return-ann (~describe "body expression or definition" e) ... (~describe "body expression" last-e)) ;; Annotate the last expression with the return type. Should be correct @@ -1240,9 +1251,16 @@ This file defines two sorts of primitives. All of them are provided into any mod #`(ann last-e #,(attribute return.type)) #'last-e)) (define d (syntax/loc stx (λ formals.erased e ... last-e*))) - (if (attribute formals.kw-property) - (kw-lambda-property d (attribute formals.kw-property)) - (opt-lambda-property d (attribute formals.opt-property)))])) + (define d/prop + (if (attribute formals.kw-property) + (kw-lambda-property d (attribute formals.kw-property)) + (opt-lambda-property d (attribute formals.opt-property)))) + ;; attach a plambda property if necessary + (if (attribute vars.type-vars) + (quasisyntax/loc stx + (#%expression + #,(plambda-property d/prop (attribute vars.type-vars)))) + d/prop)])) ;; do this ourselves so that we don't get the static bindings, diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 0398f5ce..e998cddc 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -2137,6 +2137,17 @@ (->key Univ #:y -String #t #:z -String #f -String)] [tc-e (tr:lambda (x #:y [y : String "y"] #:z [z : String "z"]) (string-append y z)) (->key Univ #:y -String #f #:z -String #f -String)] + ;; for these next two tests, test the application instead of the + ;; type of the function because the precise filters are hard to + ;; get right in the expected result type. + [tc-e ((inst (tr:lambda (x [y : A]) #:forall (A) y) String) 'a "foo") + #:ret (ret -String (-FS -top -bot))] + [tc-e ((inst (tr:lambda (x [y : A]) #:∀ (A) y) String) 'a "foo") + #:ret (ret -String (-FS -top -bot))] + #| FIXME: does not work yet, TR thinks the type variable is unbound + [tc-e (inst (tr:lambda (x [y : A] [z : String "z"]) #:forall (A) y) String) + #:ret (ret (->opt Univ -String [-String] -String) (-FS -top -bot))] + |# ;; test new :-less forms that allow fewer annotations [tc-e (let ([x "foo"]) x) -String] @@ -2148,6 +2159,10 @@ -String] [tc-e (let ([y 'y] [x : String "foo"]) (string-append x "bar")) -String] + [tc-e (let ([x : A "foo"]) #:forall (A) x) + #:ret (ret -String (-FS -top -bot))] + [tc-e (let ([y 'y] [x : A "foo"]) #:forall (A) x) + #:ret (ret -String (-FS -top -bot))] [tc-e (let* ([x "foo"]) x) -String] [tc-e (let* ([x : String "foo"]) (string-append x "bar")) -String]