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);