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

[lexi-lambda]

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.

[samth]

I think this is because Typed Racket only protects provided identifiers that are defined in "this module", and that check is missing identifiers imported with require/typed.

[mfelleisen]

I will say that I don’t understand the rationale of this design decision. Could you explain?

[samth]

It's not a design decision, it's a bug. I'm just pointing out where the bug is in the code.

[mfelleisen]

Thanks for the confirmation.