SE-0413: Typed throws

[Douglas_Gregor]

@xwu

Eek, this is a sharp edge, then, because if I delete the catch clause, (11') would throw F.e, yes?:

func n_prime() throws(F) {
  do {
    throw .e // (11')
  }
  // ...
}

Yes, that's correct.

I will continue to call your extension that permits throwing .e in an any Error context "evil"

Doug

[xwu (Xiaodi Wu)]

@Douglas_Gregor

I will continue to call your extension that permits throwing .e in an any Error context "evil"

Am I to understand, then, that without the "evil" extension, the original n() would reject type inference for the first throw .e at (11), rather than inferring F.e from the outer typed throws, because it would be in an any Error context?

I'm surprised that my other devious extension isn't a source of problems:

@xwu

func k() throws(F) {
  do throws(E) {
    throw .e // (5)
  } catch is E {
    throw .e // (6)
  }
  // ...
}

(5) throws E.e, (6) throws F.e.

If (5) throws E.e, which I deliberately made a static member returning F(), then (6) and the ellipsis are unreachable and the function unconditionally throws.

It would seem to me that the more conservative rule would be not to allow type inference at (5), since there is no static member e of type E that's defined on E, but I have to admit I have long ago forgotten the rules we settled on for leading dot type inference.

[Douglas_Gregor]

@xwu

Am I to understand, then, that without the "evil" extension, the original n() would reject type inference for the first throw .e at (11), rather than inferring F.e from the outer typed throws, because it would be in an any Error context?

Yes, that's correct.

@xwu

I'm surprised that my other devious extension isn't a source of problems:

@xwu

func k() throws(F) {
  do throws(E) {
    throw .e // (5)
  } catch is E {
    throw .e // (6)
  }
  // ...
}

(5) throws E.e, (6) throws F.e.

If (5) throws E.e, which I deliberately made a static member returning F(), then (6) and the ellipsis are unreachable and the function unconditionally throws.

Sure. A sufficiently smart compiler would warn you that the code at the ellipsis is unreachable.

@xwu

It would seem to me that the more conservative rule would be not to allow type inference at (5), since there is no static member e of type E that's defined on E, but I have to admit I have long ago forgotten the rules we settled on for leading dot type inference.

Members of protocols that E conforms to are effectively considered to be members of E, so I think this is the right general rule. It doesn't seem like changing that rule is in scope for this proposal either way, though.

Doug

[Jon_Shier]

Is there an updated toolchain we can try here? I think there have been many fixes since the original one was generated.

[wadetregaskis]

@Douglas_Gregor

The latter is not correct code, though. You would need something like catch is CatError or catch let error as CatError.

Indeed - the perils of coding on the fly in forum posts. I meant catch is CatError.

@Douglas_Gregor

Regardless, the difference stated plainly is: the do throws(CatError) formulation makes sure that nothing in the do block throws anything other than CatError, while the latter allows the do block to throw anything, but has special processing when CatError is thrown.

So if you had:

do {
    try callCats()
    try callDogs()
} catch is CatError {
    …
}

…IIRC from the proposal, that would compile and the DogError would implicitly be unhandled, passing up to the surrounding context?

I guess my mind's wandering along to parallels - or not, as the case appears to be - with switch statements and exhaustivity checking. i.e. you'd have to have an explicit default handler in the analagous switch situation, to cover DogError. I get why it's convenient to not require an explicit "default: rethrow" indication on do…catch, but it's also somewhat at odds - when working with typed errors - where you might want that level of assurance from the compiler. e.g. where you're intending to catch all error types and want the compiler to tell you if that's no longer the case because of changes inside the do block.

I get that do throws(X) nominally handles that, but it seems like to handle multiple types of errors it will require full sum-type support in the language, as opposed to potential revisions to catch clause exhaustiveness checking which could be adapted in isolation to the rest of the type system. Also, do throws(X | Y | Z) { … } catch is X { … } catch is Y { … } catch is Z { …} looks a bit redundant.

[xwu (Xiaodi Wu)]

@Douglas_Gregor

Sure. A sufficiently smart compiler would warn you that the code at the ellipsis is unreachable.

@xwu

It would seem to me that the more conservative rule would be not to allow type inference at (5), since there is no static member e of type E that's defined on E, but I have to admit I have long ago forgotten the rules we settled on for leading dot type inference.

Members of protocols that E conforms to are effectively considered to be members of E, so I think this is the right general rule. It doesn't seem like changing that rule is in scope for this proposal either way, though.

Sorry, I was referring to the following extension I wrote above:

extension E {
    static var e: F { F.e } // note this twist.
}

Inside do throws(E) { ... }, does your proposal amendment intend to permit an error of type F (not E, even if it's spelled as a static member on E) to be thrown (and uncaught) as given in the example as per your answer about (5)?

[Douglas_Gregor]

@wadetregaskis

So if you had:

do {
    try callCats()
    try callDogs()
} catch is CatError {
    …
}

…IIRC from the proposal, that would compile and the DogError would implicitly be unhandled, passing up to the surrounding context?

Yes.

@wadetregaskis

I guess my mind's wandering along to parallels - or not, as the case appears to be - with switch statements and exhaustivity checking. i.e. you'd have to have an explicit default handler in the analagous switch situation, to cover DogError. I get why it's convenient to not require an explicit "default: rethrow" indication on do…catch, but it's also somewhat at odds - when working with typed errors - where you might want that level of assurance from the compiler. e.g. where you're intending to catch all error types and want the compiler to tell you if that's no longer the case because of changes inside the do block.

I think if you want that level of assurance that you've dealt with all of the kinds of errors, you add the exhaustive catch { ... }. The answer really hasn't changed with typed throws. do throws(...) helps a little if you want to be explicit about what can be thrown, but either way you're still writing the catch { ... } to be exhaustive.

@wadetregaskis

I get that do throws(X) nominally handles that, but it seems like to handle multiple types of errors it will require full sum-type support in the language, as opposed to potential revisions to catch clause exhaustiveness checking which could be adapted in isolation to the rest of the type system. Also, do throws(X | Y | Z) { … } catch is X { … } catch is Y { … } catch is Z { …} looks a bit redundant.

I see what you mean. If we were to introduce a catch-exhaustiveness feature, we'd either have to say that feature doesn't compose well with do throws(...), extend just do throws(...) to support multiple throwing types (potentially without doing so for functions and closures), or go all the way to sum types. Personally, I wouldn't be bothered by the first one; the second would feel painfully inconsistent; and the third as intentionally a separate topic.

Doug

[Gerzer (Gabriel Jacoby-Cooper)]

I’ll echo what some other people have said: this is a great proposal, and I love how it seamlessly generalizes existing throwing and non-throwing code, interpreting them as throws(any Error) and throws(Never), respectively. I also appreciate that it recognizes that untyped throws should remain the “default”, so to speak, if there’s not a very good reason to constrain the scope of possible errors.

Language additions that effectively “de-magic-ify” existing constructs/special cases, like this one, are often the best changes because they make up for the increased language complexity with improved consistency and less magic.

[griotspeak (TJ Usiyan)]

Will catch is CatError syntax work even where typed throws wasn't involved?

If it does, do we have strong case (other than brevity) to add it instead of steering people toward case let catError as CatError? I'm asking because they look so very similar and, if we are not doing any kind of exhaustivity checking, behave the same way. It bothers me that we would add a distinct but not terribly different way to spell this.

[xwu (Xiaodi Wu)]

@griotspeak

Will catch is CatError syntax work even where typed throws wasn't involved?

It works today.

[beccadax (Becca Royal-Gordon)]

catch is CatError is an existing feature; it tests the type of the error but doesn’t capture it into a variable. It’s also refutable, meaning it represents a match that might fail.

It’s worth keeping in mind that most of catch’s behavior is derived from, and identical to, pattern matching features from case statements. catch let error as CatError and catch is CatError work the way they do because they work like case let error as CatError and case is CatError. Their design is not arbitrary, and changing them in ways that break equivalence with case patterns is not without cognitive cost.

[griotspeak (TJ Usiyan)]

Ah. I confused the issue. I am surprised that using this pattern foregoes the automatic binding to error. (that last sentence is unrelated to this proposal, just to be clear.)

Thanks for the clarification

[ellie20]

I'll repeat here a comment I made somewhere else:

@ellie20

A concern I have is that the thrown type of the function is required to conform to Error. I think there are two potential problems with that.

First, doing so unnecessarily requires any thrown type to conform to Sendable. This makes sense with Error because any Error is a "currency type", and conforming it to Sendable aids interoperability with concurrency. But with typed throws, this becomes unnecessary, since the compiler can always statically determine if a given error type is Sendable or not.

Second, we can expect some users to make "helper enums" with something like this:

enum MyError {
    case someSpecializedError
    case decoding(DecodingError)
}

In cases like these, it's almost always wrong to promote MyError to any Error, because code that would normally handle a DecodingError would fail to do so. Additionally, we might not want users to throw the .someSpecializedError case outside of some specific domain. Making MyError not conform to Error would prevent that.

With the addition that the problem with required Sendable conformance will also apply to ~Copyable, and future hypothetical opt-out protocols like ~Escapable.

[Paul_Cantrell]

This talk of do blocks got me thinking and experimenting. This is a compiler crasher in the proposal toolchain:

func f() throws(Foo) {
  do {
    throw Bar()
  } catch {
    print("Bar was barred")
  }
  throw Foo()
}

I would cautiously assume that, once the crash is fixed, this should in fact work: the compiler can recognize that the do block exhaustively handles its errors, and therefore only Foo can be thrown from the function body. Is that correct?

What about this? Should the compiler still recognize the exhaustiveness of the catch clause?

func f() throws(Foo) {
  do {
    throw Bar()
  } catch is Bar {  // ← this line changed from above
    print("Bar was barred")
  }
  throw Foo()
}

I assume, however, that this is squarely beyond what we should expect to work, because even though it’s correct code, the compiler can’t infer a narrower thrown type for the do block than any Error, and catch is Bar does not exhaustively handle that (correct?):

func f() throws(Foo) {
  do {
    if .random() {
      throw Foo()  // Thrown from function
    } else {
      throw Bar()  // Handled within function
    }
  } catch is Bar {
    print("Bar was barred")
  }
}

[xwu (Xiaodi Wu)]

@Paul_Cantrell

What about this? Should the compiler still recognize the exhaustiveness of the catch clause?

func f() throws(Foo) {
  do {
    throw Bar()
  } catch is Bar {  // ← this line changed from above
    print("Bar was barred")
  }
  throw Foo()
}

Given @Douglas_Gregor's answer to me above, the intention of this amendment is that do { ... } catch { ... } is synonymous with do throws(any Error) { ... } catch { ... }.

Therefore, by design and not due to limitations of implementation, your example isn't exhaustive because the do block "force boxes" the thrown type to any Error and catch is matching on the dynamic type of the value at runtime (notionally—as always, the compiler is free to optimize under the hood as long as the observable behavior is untouched).

[wadetregaskis]

@xwu

Therefore, by design and not due to limitations of implementation, your example isn't exhaustive because the do block "force boxes" the thrown type to any Error and catch is matching on the dynamic type of the value at runtime (notionally—as always, the compiler is free to optimize under the hood as long as the observable behavior is untouched).

But that implies that the following won't compile, because the error type will be any Error, not BarError:

do {
    throw Bar()
} catch {
    print("Bar has \(bar.someTypeSpecificProperty).")
}

…and that seems like a real bummer. It was one thing to be limited to any Error in multi-type cases, but to now rule out any type inference seems a leap too far.

[xwu (Xiaodi Wu)]

@wadetregaskis

But that implies that the following won't compile, because the error type will be any Error, not BarError:

Ah, right, and what you describe is right there in the proposal, so I'm not sure how to reconcile the two points.

[Paul_Cantrell]

@xwu

Therefore, by design and not due to limitations of implementation, your example isn't exhaustive because the do block "force boxes" the thrown type to any Error

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.

[nnnnnnnn (Nate Cook)]

This is a terrific update, and goes beyond my concern about missing type information in the catch block to add additional error type information in the do block. Thanks, @beccadax and @Douglas_Gregor!

[Douglas_Gregor]

@Paul_Cantrell

This talk of do blocks got me thinking and experimenting. This is a compiler crasher in the proposal toolchain:

func f() throws(Foo) {
  do {
    throw Bar()
  } catch {
    print("Bar was barred")
  }
  throw Foo()
}

Thank you! This was an issue with one of the compiler's internal verifiers enforcing an incorrect variant. If you're curious, the fix is here, but you should be able to work around the issue by passing -Xfrontend -disable-ast-verifier with any recent-ish toolchain.

@Paul_Cantrell

I would cautiously assume that, once the crash is fixed, this should in fact work: the compiler can recognize that the do block exhaustively handles its errors, and therefore only Foo can be thrown from the function body. Is that correct?

Yes, that is correct.

@xwu

Given @Douglas_Gregor's answer to me above, the intention of this amendment is that do { ... } catch { ... } is synonymous with do throws(any Error) { ... } catch { ... }.

Therefore, by design and not due to limitations of implementation, your example isn't exhaustive because the do block "force boxes" the thrown type to any Error and catch is matching on the dynamic type of the value at runtime (notionally—as always, the compiler is free to optimize under the hood as long as the observable behavior is untouched).

I think there was a misunderstanding here. do..catch without any throws does type inference from the do body to determine the thrown error. In other words, it infers throws(<whatever the body actually throws>). My reply to you was saying that do throws is equivalent to do throws(any Error), not that do was equivalent to do throws(any Error).

@wadetregaskis

But that implies that the following won't compile, because the error type will be any Error, not BarError:

do {
    throw Bar()
} catch {
    print("Bar has \(bar.someTypeSpecificProperty).")
}

…and that seems like a real bummer. It was one thing to be limited to any Error in multi-type cases, but to now rule out any type inference seems a leap too far.

Xiaodi's interpretation was incorrect. This does compile, because type inference infers do throws(Bar) from the do body.

@Paul_Cantrell

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

Yes, the compiler does infer the do block to be do throws(Bar). Actually, I'd like to clarify my presentation in the proposal here, by making do throws(...) the core syntax, and then layer type inference on top of it, documenting things as, e.g., do /*inferred throws(Bar)*/. As noted in the original section on catching thrown errors, we infer that this do body throws Bar in Swift 6, but for source compatibility reasons we will infer that it throws any Error in Swift 5.

@Paul_Cantrell

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.)

We intentionally don't try to evaluating catch clauses with is or as in them; the end of the section I cited above notes that the only way to get an exhaustive catch is for it to not have a refutable pattern (i.e., catch { } is okay and catch let myError is okay, but not catch is... or catch as...).

@Jon_Shier

Is there an updated toolchain we can try here? I think there have been many fixes since the original one was generated.

I kicked off a toolchain build in the PR mentioned above, which will contain all of the fixes thus far. I'll update again once the newly-proposed do throws(...) is implemented.

• macOS toolchain: https://ci.swift.org/job/swift-PR-toolchain-macos/969/artifact/branch-main/swift-PR-70182-969-osx.tar.gz
• Ubuntu 20.04 toolchain: https://download.swift.org/tmp/pull-request/70182/660/ubuntu2004/PR-ubuntu2004.tar.gz
• Windows toolchain: Swift Pull Request Toolchain Windows #1048 [Jenkins]

These include the implementation of the new do throws(...) from [Typed throws] Implement support for do throws(...) syntax by DougGregor · Pull Request #70182 · apple/swift · GitHub

[EDIT: Added toolchain links, link to PR]

[EDIT #2: Updated toolchain links to point to a toolchain that also has do throws(...) support]

Doug