a type system can be both logically consistent and expressive. the trade-off is with things like the efficiency with which it can prove the program is correct (and even the possibility that it cannot be proved at all).

what typesafety is talking about is errors. not trade-offs. that the type system says something is safe when it is not.