[plt-scheme] Contracts for polymorphic functions

The other day I was discussing with someone that contracts can't
express or enforce proper behavior of polymorphic functions (e.g.
map), but after looking at the contract.ss documentation it seems I'm
wrong.  Proper use of anaphoric-contracts should be able to achieve
this effect, but the current function contract forms don't facilitate
this very well.

For those unfamiliar, (anaphoric-contracts) produces two values - the
first, a contract which accepts all values; the second, a contract
which accepts precisely those values which have already been accepted
by the first.  I would use this to provide a contract for map in the
following way, assuming the use of (->L ...), a function contract like
(->r ...) but which takes as an extra first parameter a set of
let-values-like definitions which are evaluated at each application of
the function and are in scope for all subsequent expressions in the
contract.

  (provide/contract
   (map (->L ([(A1 A2) (anaphoric-contracts)]
              [(B1 B2) (anaphoric-contracts)])
             ([f (-> A2 B1)]
              [elems (listof A1)])
             (listof B2))))

The map contract wraps f in a function contract and checks that elems
is a list of A1 - recording each elem in the first anaphoric contract.
 The contract on f uses return contract A2 to enforce that inputs to f
only come from the list elems.  Return values from f are checked by
B1, recording them for use by B2, thus verifying in map's return
contract that all list elements were produced by f.

In some sense, this expresses the polymorphic nature of map - the
relationship between its input/output lists and the domain/range of
the given function.  My remaining questions are - was this an intended
use of anaphoric-contracts, if so why is there no existing function
contract constructor that facilitates creating new anaphoric contracts
at function invocation, and is there anything else interesting about
this I've left out?

I'm guessing this isn't a particularly efficient contract to attach to
a function, but wrapping map in a contract that checks the entire list
isn't going to be efficient so I'm not sure using fresh anaphoric
contracts is much worse of a hit.

--Carl