One thing I've really come to appreciate from working on type checkers:
There's a crucial difference between the type system and checks you can do on type-inferred code.
E.g. using a bottom type is totally well-typed, but users expect warnings:
x = exit(0);