I believe your question and Douglas’s answer about “force boxing” was in regards to do throws { … }, which is equivalent to do throws(any Error) { … }.
My question was about inferred thrown type from do { … } (note the lack of a throws):
do { // What’s inferred here?
throw Bar()
} catch is Bar {
print("Bar was barred")
}
The compiler could infer the do block to be do throws(Bar) — and the pull request seems to suggest it does — which at least opens the door to recognizing the exhaustiveness of the catch. (I rather suspect the exhaustiveness checking of catch clauses isn’t that sophisticated anyway, which is the second half of my question.)
Or the compiler could infer it to be do throws(any Error) — but I rather suspect not, since it needs to correctly infer throws(Never) in order for this to be a non-source-breaking proposal.
I’m not sure Douglas answered that particular question. Apologies if I missed it.