[racket-dev] Typed Racket and importing polymorphic code

Here's a typed module:

(module A typed/racket (provide insert map) (define insert cons))

Here are two clients, which behave inconsistently:

> (module B racket (require 'A) insert)
. Type Checker: The type of insert cannot be converted to a contract in: insert
> (module C racket (require 'A) map)

Let's instead save A to a file, and write these clients as:

-----

#lang racket
(require "typed-set-impl.rkt")

-----

F5 executes fine.  Running works:

> (map + '(1 2 3) '(4 5 6))
'(5 7 9)

But if I now type at the REPL:

> insert

I get the same error:

Type Checker: The type of insert cannot be converted to a contract in: insert

I have two issues with this:

1. Why is this discovered only when I "touch" insert and not sooner?
Is there some kind of lazy contract creation happening at run-time?

1'. That seems unlikely given that if I instead add "insert" to the
above (#lang racket) source file and run Check Syntax, I get the same
error -- so it is indeed a static error.  (Well, maybe not "static",
there are probably three or four "times" at work here.)

2. Why does the same not happen with map?  I can use map freely; if I
put it in the #lang racket file and Check Syntax, it draws an arrow
from map to the required (typed) file.  Yet in the typed file:

> insert
- : (All (a b) (case-lambda (a (Listof a) -> (Listof a)) (a b -> (Pairof a b))))
#<procedure:cons>
> map
- : (All (c a b ...) (case-lambda ((a -> c) (Pairof a (Listof a)) ->
(Pairof c (Listof c))) ((a b ... b -> c) (Listof a) (Listof b) ... b
-> (Listof c))))
#<procedure:map>

so map does not look any less polymorphic than insert....

So what on earth is going on?