That's a... very good point. We may have to reconsider this, because I certainly hadn't explicitly thought of the implications here, but maybe others had.
Assuming we don't allow retroactive overlapping conformances (as in, all conformances for a given type to a given protocol must be defined in the same module), we could retain the behaviour and it just becomes a breaking change to introduce an overlapping conformance, or, to default to safety, we'd require a non-overlapping conformance to be marked as "forever unique" or something, to indicate it can participate in such inference.
But, even then, having such overlapping conformances brings a few other things to solve; such as, what's the generic bounds of f in:
struct X<T> {}
extension X: P where T: P1 {}
extension X: P where T: P2 {}
extension X: P where T == SomeType {}
struct RequiresP<U: P> {}
func f<V>(_: RequiresP<X<V>>) {}
We'd either need to have a bound X<V>: P, or some sort of disjunction V: P1 || V: P2 || V == SomeType, neither of which we currently support (but we control the compiler so presumably we could, but extra complexity!). The former could presumably be inferred, but the latter couldn't and would thus have to be programmer-visible/writable.
The proposal does touch on the pain of having disjunctions briefly "It is no longer possible to uniquely say what is required to make a generic type conform to a protocol, because there might be several unrelated possibilities", but as you say, it doesn't explicitly cover this.
Thoughts, @Douglas_Gregor?
(Although, if we do disable that inference, that opens the way for implied conditional conformances, in my mind!)