Sadly, Typed Racket always seemed to me like some kind of shoehorning an ad-hoc system onto an AST. For that purpose, a deductive system seems much more natural. There may be problems with decidability, but the fortuitous thing is that this is not a deal-breaker for a primarily dynamic language. You should always be able to rewrite your modules so that they're easier to check, but even if you can't do that outright, the system could still find faster versions if a few type guards or other invariant checks get inserted here and there, or perhaps some form of assistant in your development environment could hint at the need to insert them manually.