Treat fully-annotated plain define as an annotated defintion.

Fixes most of PR 14702.

original commit: 2825ba142b03c8ecd6f3231d7685a2d652c6201b

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

@@ -1244,6 +1244,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
        (begin
          (: nm : type)
          (define nm body)))]
+    [(-define (nm:id . formals:annotated-formals) : ret-ty body ...)
+     (with-syntax ([arrty (syntax/loc stx (formals.arg-ty ... -> ret-ty))])
+       (syntax/loc stx
+         (-define nm : arrty
+           (-lambda formals body ...))))]
+    ;; bug 14702: the below should generate a `:` annotation when possible
+    ;; currently, the above special case does the right thing for non-curried lambdas
     [(-define vars:maybe-lambda-type-vars
               formals:curried-formals
               return:return-ann
@@ -1258,6 +1265,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
         #`(define formals.erased body ... last-body*)
         #'-lambda
         #t #t))
+     (define type-ann
+       (and (attribute return.type)))
      ;; insert in type variables if necessary
      (define rhs*
        (syntax-parse rhs

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr14702.rkt

@@ -0,0 +1,2 @@
+#lang typed/racket
+(define (f [x : Integer]) : Integer (f x))