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.
It is a little clearer to me how this works with things like primitives, but how do you annotate a function that takes a map as input and returns a list?
(defn my-keys [m]
(keys m))
