[racket] Contracts and typed regions

Hi All,

I have the following type declaration in Typed Racket.

(: next-prime :  (case-> (N -> N) (Z -> Z)) )

The function next-prime returns the next prime larger than the input.

 (next-prime  4)  evaluates to  5
 (next-prime -4)  evaluates to -3

The type captures the fact that given a natural number,
next-prime will return a natural number, but at the same
time it works for an arbitrary integer.

Now I like to use it in a non-typed piece of Racket code.
Simply requiring the module containing next-prime
doesn't work. I get this error:

  Type Checker: The type of next-prime cannot be converted to
                           a contract in: (next-prime p)

So in order to circumvent this I decide to use next-prime in a
typed region using with-type:

      (with-type #:result Number
                       #:freevars ([p Natural])
                       (next-prime p))

The type checker however gives me the exact same error even
though no contract for next-prime is needed.

So, what is the best way for me to export next-prime from
the Typed Racket code, so I can use from an untyped module?

-- 
Jens Axel Søgaard