That's a good distinction to point out, yes 
Follow-on questions/issues related to inference:
The proposal states that protocols which refine ~Copyable protocols must explicitly state non-copyability:
protocol P: ~Copyable { }
protocol Q: P { }
// `Q` is implicitly `Copyable`, which is allowed since it is "more refined" than `~Copyable`
protocol R: P, ~Copyable { }
While I understand how one arrives at this rationale, it's opposite the usual rules and therefore will inevitably catch some folks by surprise. The lack of any written artifact of the inferred copyability compounds the problem by making it harder to communicate the correct interpretation.
Also, if I understand correctly, given protocol P: ~Copyable, then for a conforming type:
struct S: P { }
...S is intended by this pitch to be Copyable using the same rationale, but it is not demonstrated explicitly in the pitch examples.
Supposing that we take the pitch as stated such that S is implicitly Copyable just as Q is, what of the following?
struct T<U: P> { } // `U` is constrained to `P: ~Copyable`
By the logic of constraints, U must not be implicitly Copyable; rather, U: P implies U: ~Copyable even though Q: P above implies Q: P, Copyable. Tricky, but learnable.
Then, by the inference rules pitched here, T: ~Copyable because U: ~Copyable (even if nowhere is there a tilde in the declaration).
However, if instead I declare struct T2<U: Q>, then since Q is implicitly unconditionally Copyable, T2 is also implicitly unconditionally Copyable. Or to put it together:
protocol P: ~Copyable { }
protocol Q: P { } // Copyable
struct T<U: P> { } // ~Copyable
struct T2<U: Q> { } // Copyable
For three declarations that each use what's superficially the same :, my feeling is that there are too many interacting rules of inference at play here.
Ah, and I forgot—we have primary associated type notation for protocols now: since those aren't generics per se, things look similar but then diverge...
struct S<T> where T: ~Copyable { }
// `S` is implicitly `~Copyable`, per pitch
protocol PP<T> where T: ~Copyable { associatedtype T }
// ...equivalent to:
protocol PP<T> { associatedtype T: ~Copyable }
// `PP` is implicitly `Copyable`, per pitch
I'm wary of this amendment and of this interpretation of SE-0390.
A protocol which is Copyable can refine a protocol which is ~Copyable and a generic type that is ~Copyable can be conditionally Copyable. Thus the syntax ~Copyable very much does not mean "without Copyable" in those contexts. Rather, there is a relationship whereby Copyable refines ~Copyable—if we wanted to stick with your terminology, we could perhaps say that ~Copyable is read "without Copyable yet."
We allow—even require, in the case of conditional conformances—writing out multiple refining requirements such as T: Sequence, T: Collection; and I see no reason to ban this particular one here.
Overall, I have no doubt we can keep patching special rules upon special rules to try to make each individual example work, but it doesn't feel like the best direction for getting to a workable whole.
While I am reasonably happy with the ~Copyable spelling we ended up at in SE-0390, I would urge us not to regard this as some special operator that needs exegesis and new semantics. I'd be curious how far we get if instead we replace ~Copyable in one's mind's eye with a run-of-the-mill spelling such as PossiblyNoncopyable and consider what falls out from existing rules when we have protocol Copyable: PossiblyNoncopyable { }; typealias Any = any Copyable, then add the minimum inference rules we need so that existing types written for Swift 5 are inferred to conform to Copyable.
