> If a function is annotated f: T -> U where U is not an error, the contract with the caller is that f does not error, and cannot be changed to produce an error, and the compiler upholds this contract for all callers and definitions or redefinitions of f
The OP is not suggesting that. They're suggesting that U can be an extensible union type that can be inferred from the code. Of course, if you declare it to not be such a union, then you guarantee no errors.
Just think of it like checked exceptions from Java, except the exception signature is inferred from the function's code. If you explicitly declare "does not throw", then the compiler produces a type error that you have not handled all exceptions.
The OP is not suggesting that. They're suggesting that U can be an extensible union type that can be inferred from the code. Of course, if you declare it to not be such a union, then you guarantee no errors.
Just think of it like checked exceptions from Java, except the exception signature is inferred from the function's code. If you explicitly declare "does not throw", then the compiler produces a type error that you have not handled all exceptions.