Erlang and Elixir have long had "dialyzer" as a type checker. The problem is that it had some severe limitations in approach (and implementation) and so the cost/benefit ratio wasn't great.

This article really speaks to how they're thinking about the costs of the type system, so that you mostly get benefit, and that's great.