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.