I'm happy to keep using this thread until I'm ready to pitch the new approach.
A few of us have tossed around what this might look like, and our thoughts aren't that different from yours, although some of the conclusions are a little different. I think we do have to think of a re-borrow as being effectively a copy. What we have, then, is a type that semantically permits multiple copies to exist as long as they are guaranteed to be used exclusively with each other. That's a potentially broad class of types, although the fact that destruction has to be coordinated somehow does limit its usefulness.[1] Perhaps this could be an ExclusiveCopyable marker protocol, sitting between ~Copyable and Copyable.
Enforcing this restriction doesn't technically require the type to be ~Escapable: we can enforce it locally as long as the copies remain local. However, that seems pretty pointless, because the programmer might as well just have one local value; therefore, we might as well require non-escapability. Once we're doing that, we can just require the type to originate a lifetime restriction that we can limit. We don't need to, or even want to, restrict all component lifetimes, though.
Since re-borrows are copies, yes, we have to think about when we copy the component values. borrowing, mutating, and consuming are all still useful here, but we do run into the problem that making the exclusive operations consuming would imply that they all do a primitive value copy. That leads me back to thinking we still need an exclusive access specifier in the long term. In the short term, since the types we immediately care about all look like MutableSpan (i.e. small types with trivial components), there's no harm in just using consuming. Specifically, since ExclusiveCopyable + consuming would let us eanble the desired use patterns for MutableSpan, we should clearly do that first and then only consider exclusive ownership later if there's a demand for it.
MutableSpan et al. also have the characteristic that we should probably default to passing them around with consuming or exclusive ownership. That is probably not generally true of all ExclusiveCopyable types, though, so if we want to add such a rule, we should do so separately.
Maybe if we had a "copy constructor" that could make destruction dynamically a no-op for nested copies? ↩︎