How does your approach compare to Typed Racket and Typed Clojure? Could they conceivably achieve the same performance or is there a fundamental difference?
Typed Racket also includes more types, like ": Integer [more precisely: Negative-Fixnum]" (from docs), as well as polymorphic data structures and higher-order functions. I don't know if this is a "fundamental difference" but it might mean Facebook's type checker can optimize in certain ways that Racket's cannot.
The Typed Racket type checker is much slower than Hack, though.
Hack does seem to have polymorphic data structures and higher-order functions.