Better error msg for annotations on unbound ids

Closes PR 14246

Please merge to v6.0

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

@@ -1,7 +1,8 @@
 #lang racket/base
 
 (require (for-syntax racket/base syntax/parse unstable/sequence unstable/syntax
-                     "../utils/disappeared-use.rkt")
+                     "../utils/disappeared-use.rkt"
+                     (only-in "../utils/tc-utils.rkt" tc-error/stx))
          "../typecheck/internal-forms.rkt"
          (prefix-in t: "base-types-extra.rkt"))
 
@@ -44,7 +45,10 @@
     [(_ top-level? i:id ty)
      (unless (or (syntax-e #'top-level?)
                  (identifier-binding #'i))
-       (raise-syntax-error #f "unbound identifier in module" #'i))
+       (tc-error/stx #'i
+                     "Declaration for ~a provided, but ~a has no definition"
+                     (syntax-e #'i)
+                     (syntax-e #'i)))
      (syntax-property (syntax/loc stx (begin (quote-syntax (:-internal i ty))
                                              (#%plain-app values)))
                       'disappeared-use #'i)]

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/pr14246-2.rkt

@@ -0,0 +1,12 @@
+#;
+(exn-pred #rx"Type Checker: Declaration for n provided, but n has no definition")
+#lang typed/racket
+
+;; Similar to pr14246.rkt, but for local definitions
+(: foo : Number -> Number)
+(define (foo a)
+  (: n : Number)
+  (: i : Integer)
+  (: s : String)
+  a)
+

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/pr14246.rkt

@@ -0,0 +1,8 @@
+#;
+(exn-pred #rx"Type Checker: Declaration for n provided, but n has no definition")
+#lang typed/racket
+
+;; Test for the error message for unbound module bindings
+;; with type annotations
+(: n String)
+