There would be annotations in the same places as Typed Clojure, except :no-check would be replaced by type soundness-preserving runtime assertions. There would be no need for :no-check anyway; Typed Racket's base annotations are complete AFAIK.
Edit: Just found Seqable. Looking into it now. This link helped me a lot. https://github.com/clojure/core.typed/wiki/Types
(ann my-keys (All [a] [(t/Map a Any) -> (t/Coll a)])