So formalizing things with type systems is great. In fact, I'm a huge proponent of it.
The problem still remains, you may not have a sufficiently well developed requirement set to be able to specify things in your type system.
I'll give an example: It's possible in Haskell (really many languages) to create a type SafeString which can be constructed from a standard String and does all the necessary escaping for the target (let's say it takes in a username and works to prevent sql injection attempts, or removes HTML tags, or whatever might be appropriate). And for all practical purposes it behaves exactly like a string otherwise. Any time you want to make a SQL query or generate some HTML you know that you can use a SafeString and it'll (barring errors in implementation) work without causing you either security risks or producing incorrect outputs.
That's fine that we can do this, if it doesn't make it into your system design you won't know that you need to do this.
The type system itself doesn't tell you that your types are underspecified. It needs to come from the requirements analysis (in this case, requirements as viewed through a security-oriented perspective). But type systems allow you to encode that specification once it's been made.