However, there's one very important language design difference between this and Java-styled checked exceptions: using sum type gives you effect polymorphism for free. This means you can write (say) a map function which says it has precisely the same exception type of its argument function, using the same machinery you're using for generics everywhere else.
This is a big from the usability side, since AFAICT it was the lack of effect polymorphism that turned people off of Java-style checked exceptions. From a language implementation standpoint, it's also nice not to have to implement type inference twice, once for return values and once for exceptions. :)