Enable mixed type annotations for define

original commit: 3d177e454ea3634060a4b9b0814f588bc7c74e49

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt

@@ -415,30 +415,6 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ arg tys ...)
      (type-inst-property (syntax/loc #'arg (#%expression arg)) #'(tys ...))]))
 
-(define-syntax (define: stx)
-  (syntax-parse stx #:literals (:)
-    [(define: (nm:id . formals:annotated-formals) (~describe "return type annotation" (~seq : ret-ty)) body ...)
-     (with-syntax ([arrty (syntax/loc stx (formals.arg-ty ... -> ret-ty))])
-       (syntax/loc stx
-         (define: nm : arrty
-           (lambda: formals body ...))))]
-    [(define: nm:id ~! (~describe ":" :) (~describe "type" ty) body)
-     (identifier? #'nm)
-     (with-syntax ([new-nm (type-label-property #'nm #'ty)])
-       (syntax/loc stx (define new-nm body)))]
-    [(define: tvars:type-variables nm:id : ty body)
-     (with-syntax ([type (syntax/loc #'ty (All (tvars.vars ...) ty))])
-       (syntax/loc stx
-         (begin
-           (: nm : type)
-           (define nm body))))]
-    [(define: tvars:type-variables (nm:id . formals:annotated-formals) : ret-ty body ...)
-     (with-syntax ([type (syntax/loc #'ret-ty (All (tvars.vars ...) (formals.arg-ty ... -> ret-ty)))])
-       (syntax/loc stx
-         (begin
-          (: nm : type)
-          (define (nm . formals.ann-formals) body ...))))]))
-
 (define-syntax (lambda: stx)
   (syntax-parse stx
     [(lambda: formals:annotated-formals . body)
@@ -1227,6 +1203,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
              #:attr erased
              (template ((?@ . mand.form) ... (?@ . opt.form) ... . rest.form))))
 
+  (define-syntax-class curried-formals
+    #:attributes (erased)
+    #:literals (:)
+    (pattern fun:id #:with erased #'fun)
+    (pattern (fun:curried-formals . formals:lambda-formals)
+             #:with erased #`(fun.erased . #,(attribute formals.erased))))
+
   (define-splicing-syntax-class return-ann
     #:description "return type annotation"
     #:literals (:)
@@ -1262,12 +1245,63 @@ This file defines two sorts of primitives. All of them are provided into any mod
             #,(plambda-property d/prop (attribute vars.type-vars))))
          d/prop)]))
 
+;; for backwards compatibility, note that this only accepts formals
+;; with type annotations and also accepts type variables differently
+;; than -define
+(define-syntax (define: stx)
+  (syntax-parse stx #:literals (:)
+    [(define: (nm:id . formals:annotated-formals) (~describe "return type annotation" (~seq : ret-ty)) body ...)
+     (with-syntax ([arrty (syntax/loc stx (formals.arg-ty ... -> ret-ty))])
+       (syntax/loc stx
+         (-define nm : arrty
+           (-lambda formals body ...))))]
+    [(define: nm:id ~! (~describe ":" :) (~describe "type" ty) body)
+     #'(-define nm : ty body)]
+    [(define: tvars:type-variables nm:id : ty body)
+     #'(-define nm #:forall tvars : ty body)]
+    [(define: tvars:type-variables (nm:id . formals:annotated-formals) : ret-ty body ...)
+     #'(-define (nm . formals) #:forall tvars : ret-ty body ...)]))
 
-;; do this ourselves so that we don't get the static bindings,
-;; which are harder to typecheck
 (define-syntax (-define stx)
-  (define-values (i b) (normalize-definition stx #'-lambda #t #t))
-  (datum->syntax stx `(,#'define ,i ,b) stx stx))
+  (syntax-parse stx #:literals (:)
+    ;; the first two cases are actually subsumed by the last,
+    ;; but manually expanding to using the : annotation form
+    ;; produces better error messages on duplicate annotations
+    [(-define nm:id return:return-ann body)
+     (define/with-syntax maybe-ann
+       (if (attribute return.type)
+           #'(: nm return.type)
+           #'(void)))
+     (syntax/loc stx (begin maybe-ann (define nm body)))]
+    [(-define nm:id vars:lambda-type-vars : ty body)
+     (define/with-syntax type
+       (syntax/loc #'ty (All vars.type-vars ty)))
+     (syntax/loc stx
+       (begin
+         (: nm : type)
+         (define nm body)))]
+    [(-define formals:curried-formals
+              vars:maybe-lambda-type-vars
+              return:return-ann
+              body ... last-body)
+     ;; have to preprocess for the return type annotation
+     (define/with-syntax last-body*
+       (if (attribute return.type)
+           #`(ann last-body #,(attribute return.type))
+           #'last-body))
+     (define-values (defined-id rhs)
+       (normalize-definition
+        #`(define formals.erased body ... last-body*)
+        #'-lambda
+        #t #t))
+     ;; insert in type variables if necessary
+     (define rhs*
+       (syntax-parse rhs
+         #:literals (-lambda)
+         [(-lambda formals . others)
+          (template (-lambda formals (?@ . vars) . others))]
+         [_ rhs]))
+     #`(define #,defined-id #,rhs*)]))
 
 (define-syntax (with-asserts stx)
   (define-syntax-class with-asserts-clause

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt

@@ -2149,6 +2149,18 @@
              #:ret (ret (->opt Univ -String [-String] -String) (-FS -top -bot))]
        |#
 
+       ;; test `define` with mixed type annotations
+       [tc-e (let () (tr:define y "bar")
+                     (tr:define x : String "foo")
+                     (string-append x y))
+             -String]
+       [tc-e (let () (tr:define ((f [x : String]) y) x)
+                     ;; FIXME: does not work due to a bug in
+                     ;; lambda type-checking
+                     ;(tr:define ((g x) [y : String]) y)
+                     (string-append ((f "foo") 'y) "bar"))
+             -String]
+
        ;; test new :-less forms that allow fewer annotations
        [tc-e (let ([x "foo"]) x) -String]
        [tc-e (let ([x : String "foo"]) (string-append x "bar"))