[plt-scheme] Typed Scheme polymorphic variadic functions

This morning's chatter about srfi/1 motivated me to try writing some
of my favorite srfi/1 functions in typed scheme, and, while things
generally went smoothly, I haven't been able to really understand the
type signatures for polymorphic variadic functions. There is the one
example of map in the documentation, but I'm not sure I can look at it
from any more angles trying to divine its secrets.

An example of where I'm stumbling:

;; Make a heterogenous list from an argument list.
(: listf (All (A ...) (A ... A -> (List A ... A))))
(define (listf . xs)
  xs)

I'd like to understand how to write that signature, but, even more
generally, I'm confused about the "A ... A" syntax here. In the
example of the map function, there is the, to me, even more mysterious
notation
(Listof A) (Listof B) ... B

which leaves me unclear how the ellipses and the type variable relate
to each other when binding type variables. For instance, if B is a
list of type variables, then the addition of the implied Listof type
constructors is somewhat magical. My guess is that the form is
something like "Pattern ... V" where V is a free variable in Pattern.
Unfortunately, that doesn't seem to be the case in the listf type
signature above, unless I'm running afoul of a precedence issue. Is
there somewhere else I can find more explanation of this syntax?

Anthony