Disable occurrence typing for top-level variables

Closes PR 14121

original commit: 3e2911d30f4efe4901d9626e83126d7bafa55922

pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl

@@ -150,3 +150,10 @@ modification of a variable does not invalidate Typed Racket's
 knowledge of the type of that variable.  Also see
 @Secref["using-set!"  #:doc '(lib "scribblings/guide/guide.scrbl")].
 
+Furthermore, this means that the types of @rtech{top-level variable}s
+in the @gtech{REPL} cannot be refined by Typed Racket either. This is
+because the scope of a top-level variable includes future top-level
+interactions, which may include mutations. It is possible to work
+around this by moving the variable inside of a module or into a local
+binding form like @racket[let].
+

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/lexical-env.rkt

@@ -78,7 +78,9 @@
      #:declare i (expr/c #'identifier?)
      #:declare env (expr/c #'prop-env?)
      ;; check if i is ever the target of a set!
-     #'(if (is-var-mutated? i)
+     ;; or is a top-level variable
+     #'(if (or (is-var-mutated? i)
+               (not (identifier-binding i)))
            ;; if it is, we do nothing
            env
            ;; otherwise, refine the type

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

@@ -0,0 +1,14 @@
+#;
+(exn-pred #rx"Expected Number, but got \\(U Integer String\\)")
+#lang racket/load
+
+;; Test for PR 14121
+;; Top-level variables cannot be refined with occurrence typing
+;; because it's not possible to detect future set!s reliably
+
+(require typed/racket)
+
+(: x (U Integer String))
+(define x 3)
+(define f (if (integer? x) (lambda () (add1 x)) (lambda () 3)))
+