Reproviding an identifier imported with require/typed does not enforce negative obligations with contracts

This program produces a surprising result:

#lang racket

(module a racket
  (provide f)
  (define (f x) (- x 100)))

(module b typed/racket
  (require/typed
   (submod ".." a)
   [f (-> Number Number)])
  (provide f))

(require 'b)
(f #f)

I would expect it to signal a contract violation and blame the outer module, using the contract from the interface for f established by module b. However, it does not. Instead, it simply invokes f with #f, and - raises an error.

It seems like identifiers imported with require/typed are not properly protected with additional contracts if they are reprovided. I don’t think this can cause any actual unsoundness in typed code, but it’s certainly surprising.

Start by running the self-contained Typed Racket program in the issue and tracing the require/typed import followed by the reprovide from module b. Investigate how contracts are attached when imported identifiers are reprovided. Done means calling f with #f produces a contract violation blaming the outer module, with regression coverage for this example.