[racket-dev] Typed Racket and ADTs

How do I define an ADT?  Eg, I want to provide this:

(provide insert check empty-set)

(define-type RealSet (Listof Real))

(: empty-set RealSet)
(define empty-set empty)

(: insert (Real RealSet -> RealSet))
(define insert cons)

(: check (Real RealSet -> Boolean))
(define (check e s)
  (if (member e s)
      true
      false))

I see that using the opaque form of require/typed I can import RealSet
as, say, type RS and truly hide its representation.  However, this:

1. doesn't have a counterpart for *untyped* code;

2. seems very ugly to do from a typed module: I seem to need to define
the new opaque type, then enumerate everything (that I want) exported
from the typed module.  Surely there's an easy way of saying

  import SetADT renaming RealSet to RS making it opaque

?  It seems natural, but I can't figure out how to say this.

Overall, the status of representation-hiding in Typed Racket seems
rather weird.  I find it odd that even programming entirely in Typed
Racket, representations leak by default.  Worse, If I'm writing a
module whose representations I expect to frequently change, and would
like user code to avoid inadvertently relying on them, there appears
to be nothing I can do (without providing a wrapper that simply
re-exports everything with the type made opaque -- and even then, it's
not clear how to hide access to the original).  Just as there's an
opaque require, why isn't there dually an opaque provide, so the
creator can decide to hide reps?  Even if opaque provide only worked
for other typed clients, that would be a big step up.

Shriram