Different kind of checked exceptions - Guarantee to only throw X

Question

It is a widely held position that checked exceptions as implemented in Java are a bad idea. If you mark a method as throwing, calling code has to either catch the exception, or be marked as throwing, too. For this reason, it is said that exception specifications are contagious. Consequently, they are being removed from C++ (with exception of noexcept).

I wonder if you could implement a different kind of checked exceptions. Instead of "Caller must catch this", they would mean "I will only ever throw this".

The calling scope will not have to be changed at all. It is helps me as a writer of the called function to understand what I will possibly throw - if I decide to add an annotation. It would also allow the possible exceptions to be shown during code completion. I could imagine special fatal exceptions will always be allowed, like OutOfMemoryException, or Python's KeyboardInterrupt.

For example (pseudocode):

// simple case (could actually be inferred)
string lookupString(string key) throws only KeyError {
    return m_map[key];
}

// complex failing example
string readFromFile(string filename) throws IndexError {
    File f = File.Open(filename);
    return f.readline();
}
// -> Compilation error:
// File.Open may cause IOError, but readFromFile guarantees to only throw IndexError
// (optional:)
// readFromFile suggests it will throw IndexError,
// but no operation in it may possibly throw IndexError.

In case you give no specification, I would suggest to allow any exception (throw Throwable). I imagine adding this feature to an existing language, and this would be the only backwards-compatible option. For a new language, you think about a different default.

To deal with legacy code (in an external library), there could be a way to tell the compiler that a certain function or block of code only can ever throw certain exceptions. Conceptually a bit like unsafe in C#:

I swear throws only ParseError {
    return JSON.parse(json);
}

I am not aware of any language that implements this weaker kind of checked exceptions. It seems to me they would have a lot of benefits, but without the drawbacks of Java's checked exceptions. Are there any reasons that this idea wouldn't work? Has any language successfully implemented this, or tried and failed?

(Note, please do not read this as a question looking for a language recommendation and then close it. This is a question about language design, I would like to understand the benefits and drawbacks of this approach better. Possible answers I could imagine would be: "Yes, this has been attempted in language XY, but doesn't work very well because of interplay with generics." or "No, this has never been implemented, but it is a great idea. Because of <language-theoretic argument>, this can be implemented in a sound type system. See this work of Foobar for more information.")

Answer 1

Has been done in Vala.

The caveat is that not handling the exceptions in code is a compile-time warning, the idea being that one of the main issues with java checked exceptions is that when prototyping, people tend to catch and ignore the exceptions rather than considering proper error handling. If the error does occur at runtime and has not been handled in code, the default handling logic in Vala is to immediately exit.