Two soundness holes casting isolated conformances (SE-0470)

[KeithBauerANZ]

Description

The new functionality of the cast operators to dynamically fail if not called on the main actor is currently unimplemented (#82539), but even if this is implemented, there's still two problems casting isolated conformances.

Reproduction

The first problem is where a type has an isolated conformance to a protocol which inherits from Sendable:

import Dispatch

protocol P: Sendable {
    func f()
}

@MainActor
struct S: @MainActor P {
    func f() {
        MainActor.preconditionIsolated()
    }
}

@MainActor
func example(_ s: any Sendable) {
    let p = s as! any P // on the main actor, so the cast is allowed dynamically
    DispatchQueue.global().async {
        p.f() // oops, sent it anyway
    }
}

example(S())
dispatchMain()

I believe isolated conformances should be disallowed in this case.

The second problem involves sending the result of a cast:

import Dispatch

protocol P {
    func f()
}

@MainActor
struct S: @MainActor P {
    func f() {
        MainActor.preconditionIsolated()
    }
}

@MainActor
func example(_ s: sending Any) {
    let p = s as! any P // cast is dynamically OK
    Task.detached {
        p.f() // oops, sending
    }
}

example(S())
dispatchMain()

I don't see how to resolve this without having the cast operators join the result to the calling function's region, which is definitely source-breaking in some circumstances.

Expected behavior

SE-0470 shouldn't leave soundness holes

Environment

swift-driver version: 1.127.5.3 Apple Swift version 6.2 (swiftlang-6.2.0.10.950 clang-1700.3.10.950)
Target: arm64-apple-macosx15.0

Additional information

No response

[DougGregor]

The first hole is detected by newer Swift runtimes, which will (correctly) reject the cast and trap with:

Could not cast value of type 't.S' (0x1023c8190) to 't.P' (0x10450d278).

The second one is definitely a hole and needs more thought, nice find!

[DougGregor]

Current thinking on the second one:any dynamically-acquired conformance (e.g., one that comes through a dynamic cast to an existential) to a non-SendableMetatype protocol within a non-@concurrent function is tied to the current actor or the task’s region. That models the notion that we might have picked up an isolated conformance.

[KeithBauerANZ]

I don't understand why the first would fail to cast, it's being cast on the actor of the isolated conformance? It seems like isolated conformance to a protocol which requires Sendable just doesn't make sense & should be statically disallowed?

[DougGregor]

I don't understand why the first would fail to cast, it's being cast on the actor of the isolated conformance?

It's because once you have it as an any P, where P inherits Sendable, you could carry the conformance into another isolation domain and cause a data race.

It seems like isolated conformance to a protocol which requires Sendable just doesn't make sense & should be statically disallowed?

I'll add a warning here, because it's somewhat pointless to have an isolated conformance like this (you can't use it generically), but it's not "wrong" per se.