The original Gradual Typing paper by Siek and Taha actually proposes that gradual typing systems inject dynamic checks on downcasts from any. I think that’s what TypedRacket does.

The Erlang/Elixir implementations I know (e.g. Gradient / Gradualizer), however, don’t do it. I think it’s because of two reasons:

1. The implementations are independent of the compiler(s), so they have no way to inject code.
2. The type system is still advantageous if we only use static types (that is some bugs do get detected at check time, not at runtime) and it doesn’t degrade below the guarantees offered by the runtime anyway (for as long as the supervision tree is there no critical failures can bring the system down).

IMO that’s a nice blend of dynamism and ahead of time warnings.

One thing that jumps out (besides the unusual code formatting) is that the resulting type system considers code like bad/1:

1-s2.0-S2590118421000551-fx1031_lrg2196×204 27.1 KB

to be typed correctly, due to how it handles “downcasting” from any.