This is intriguing to me, because it suggests a way to accomplish the goal of a smooth migration by going in a contrary direction to this pitch.
To back up a bit: One thing that concerns me about the pitch is that we already have two special-case elisions allowed by SE-0355: Any is equivalent to any Any, and AnyObject is equivalent to any AnyObject—if we adopt this pitch as-is, then we would have a scenario where everywhere a bare protocol P means some P except for Any and AnyObject. That much can be taught but seems...inelegant.
I'm not sure if I'm reading you correctly where you talk about a "targeted carve-out," but if this is to say that for an imported Objective-C protocol ObjcP, bare ObjcP should mean any ObjcP, but for a Swift-native protocol SwiftP, bare SwiftP should mean some SwiftP—well, it would seem to me that this would make the language and our migration story more confusing, as we'd be extending the special rule above beyond just two cases that the user can memorize to arbitrarily many protocols that users have to consult documentation and/or rely on tooling to clarify the provenance of.
However, there is something particular about Objective-C protocols, shared in common with Error and with marker protocols, which bears considering: namely, in these cases, the existential types conform to the corresponding protocol. I'd argue that it makes the distinction between any P and some P less salient to the end user, since of course in those particular cases any P is notionally a valid underlying concrete type where a function expects an argument or returns a value of opaque type some P.
Indeed, one might argue that in those cases specifically the distinction shades closer to being a compiler implementation detail that the user shouldn't have to worry about unless they want to. It's a very "Swifty" thing to apply a progressive disclosure approach in such scenarios; for example, we envision that users shouldn't be required to deal with ownership operators if they're using copyable types unless they want to fine-tune their code for performance.
Therefore, if we decide not to go in the direction of this pitch, an alternative could be to roll back the requirement for explicit any specifically for "self-conforming protocols" (i.e., Obj-C protocols, Error, and marker protocols, of which we have only Sendable). In those cases, bare P would continue to mean any P, with the compiler being free as it now is to optimize provably unnecessary uses to be equivalent to some P.
In the case of your migration example, this would eliminate over half of the required edits.
This would also have the salutary benefit of allowing us to stage in the proposed "flip" in overload resolution rules discussed above in a less invasive way, although this may also be too clever by half:
For "self-conforming protocols," it is arguably the case that existential P (being notionally a valid underlying concrete type) is "more specific" than some P, aligning with present-day overload resolution rules. We could therefore say that only any P when spelled out as such is regarded in Swift 6 as being "less specific" than some P, because the former explicitly specifies an existential box, leaving any continued valid uses of bare P as "more specific."