(define) erases typechecker's knowledge of assertions

What version of Racket are you using?

v6.12

What program did you run?

#lang typed/racket

(: bytes->integer (-> Bytes Integer Integer Integer))
(define (bytes->integer a b c) 0)

(struct dummy ())
(define-type value (U dummy Integer))

(: eval-op-read-memory (-> value value value))
(define (eval-op-read-memory ptr os)
  (assert ptr exact-integer?)
  (assert os exact-integer?)
  (define bs #f)
  (bytes->integer (bytes) os os))

This program produces an error. If the (define bs #f) is commented out, the program typechecks without error.

What should have happened?

The type-checker should not throw an error, because the unused bs should not affect available type information.

Instead, either:

• The error should say that the (define) is not at the beginning of the function scope, or
• The program should compile without error.

The program compiles successfully if any of these occur:

• The (define) is moved to the beginning of the block, or removed.
• value is changed to (define-type value (U Integer))
• The asserts are moved into a with-asserts form.

If you got an error message, please include it here.

a.rkt:14:26: Type Checker: type mismatch
  expected: Integer
  given: value
  in: os

a.rkt:14:29: Type Checker: type mismatch
  expected: Integer
  given: value
  in: os

Start with the minimal typed/racket program in the issue and trace how the typechecker handles local define forms after assert-based refinements. Reproduce the reported mismatch, then verify that the unused definition no longer erases the assertions' type information or that the diagnostic clearly identifies the unsupported placement.