> the compiler can see them and prove that they match and will never be triggered

This is a huge challenge for a C-like language with pervasive global state. Might be more feasible for something like Rust, but still very difficult.

You only need to check between caller and callee. If their constraints always match, it can't be triggered, if they contradict always, it will be triggered, else it can't be decided and the programmer can add annotations if he cares about, or the compiler can check what it would be like if the caller is inlined into his calling functions if that is trivial enough.