Can't wait for this! So glad you're tackling this issue!
This detail sounds really useful to me, even outside the context of this pitch:
… to facilitate the transition of conformances from
next()tonextElement(), we add a new availability rule where the witness checker diagnoses a protocol conformance that uses an deprecated, obsoleted, or unavailable default witness implementation.
I have my own use cases for this very feature. I'll be really glad that inheriting deprecated defaults will be diagnosed as a warning.
On the isolated actor parameter:
I see there are some overlapping ideas with @John_McCall's pitch "Inheriting the caller's actor isolation".
Do you plan to integrate more parts of that pitch? Like, to use = #isolation as a default argument for nextElement or even the @inheritsIsolation attribute? If not, could you enlighten us?