[loglog]

The plain Java equivalent of the proposed semantics would be a type system extension similar to JSpecify: @Result(ok=Ok.class, error={Checked1.class, Error2.class}) Object function() combined with enough restrictions on the usages of results of such methods (e.g., only allow consuming the results in an instanceof pattern matcher; not even switch would work due to impossibility of exhaustiveness checking).

The one feature that the proposed Kotlin error types share with Java checked exceptions is that they can be collected in unions. However, the union feature for checked exceptions is pretty much useless without the ability to define higher order functions that are generic over such unions, which is why checked exceptions fell out of favor with the spread of functional APIs in Java 8.

[ajrouvoet]

This last point is the key observation.