# [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