> However, it's possible to have a more lenient static type checker that only looks for cases where you're guaranteed to get an illegal operation at runtime. They answer the question "is this definitely wrong?"

If you're thinking about Erlang's Dialyzer, almost everyone I've heard talking about it says that it's difficult to understand and doesn't provide as much confidence as a regular type system would.