How does this rule work in regard of ambiguity?

It's overloading rather than shadowing, since the two entities have different types. You can even select between them with as (well, usually).

It's also potentially important for retroactive conformances, and for library evolution, but if we really cared about that we'd allow you to define overloads of properties all the time. We might need to look into that at some point.

That's true of any overloading or shadowing, yeah.

Members of concrete types are considered "better overloads" than members of protocols.

Yep, totally! Except for the part where this changes the behavior of existing code, so we'd have to be very careful about it. This is considered part of [SR-522] Protocol funcs cannot have covariant returns.