I'd extend 1 to include "can I easily avoid subverting this type system?" Guarantees are better, but as long as I can get help that's enough for a tool to be useful assuming 2.
Regarding 2, I've long complained that the conception of types embedded in many systems (and many heads) is very representational and most of the time we don't actually care about representation. The exceptions I typically mention are where we care a lot about performance, and at system boundaries. We can fit those into your analysis by asserting (reasonably, I think) that in those instances representation starts to be a part of your problem domain.
I'd also extend 1 to include "can I subvert this type system when I really need to?"
(And to those who would say "You never need to", I don't think you can be quite that dogmatic. The real world includes a lot of unforeseen scenarios...)
Aha! I will counter that you never actually want or need to break the type comprehension of your executable but the static analysis of the compiler or dynamic analysis at runtime may be inaccurate with regards to the truth and motivate you to try and subvert it. This may be about what you were thinking when you wrote your comment but I wanted to highlight a small but important difference. I may find a useful bitwise function that takes arguments of type int and really want to execute the same bitwise function on a pair of doubles, in this case the actual type of data I want the function to operate on is "a series of bytes" but the compiler/whatever's typing system may force me to declare the function as taking an IEEE 754 or two's complement integer instead.
In these cases the typing system is constraining you from declaring a type safe operation the right way by forcing you to play within a subset of the universe of valid types.
Imagine that you have a binary-only third-party library, one function of which returns an opaque type. Imagine that you want to unpack that and observe the state of some data inside it (perhaps guided by online hints), and the vendor won't give you the ability to do so because 1) they're busy, or 2) they want a lot of money, or 3) they're out of business. You don't want to have to subvert the type system, but you still kind of need to.
And if you're going to tell me that the only reason you need to in this scenario is because the third-party vendor didn't do their job (including creating the types) right, I'd agree. That doesn't actually change what you need to do, though.
I agree, but in that case you're fighting against the typing system more than typing itself, whatever you are doing with that thing and however you would abstractly define that type (maybe as "We expect this thing to have the type of the thing that terrible third party library usually gives us back") you will make assumptions based on the fact that that value is actually one of those and you never want those assumptions violated. In this case the typing system is too restrictive and it might be a case where duck-typing would come in handy (since you can usually post-apply types in that sort of a setting).
It's an important question. Systems where you can't ever subvert the type system may be useful in some places (sandboxing) where systems with an escape hatch aren't, and maybe vice-versa (plausibly "in theory", certainly "in practice" IME). The two might be variants of the same underlying language, though - Safe Haskell is at least an attempt in this space; I don't know how well it delivers.
I've always felt type coercion is a pragmatic recognition of a lack of time, but also a lack of analysis and abstraction. If you are type coercing in an existing body of code, you probably walked into an ill-understood quirk in the key information model, or a change in circumstance.
If you are routinely coercing types in new code, you haven't done enough design and analysis. Something is off-key.
Regarding 2, I've long complained that the conception of types embedded in many systems (and many heads) is very representational and most of the time we don't actually care about representation. The exceptions I typically mention are where we care a lot about performance, and at system boundaries. We can fit those into your analysis by asserting (reasonably, I think) that in those instances representation starts to be a part of your problem domain.