Subtyping requires a theory of failure

Most type system research is built on the assumption of a clean exit. You write a function, it returns a value, the program moves on. This is the comfort zone of strict evaluation.