I think the underlying principle here is that
a function returning an opaque result type must return a value of the same concrete type
Tfrom eachreturnstatement
is a condition that does not have to apply across executions of the same program, the same way that Hashable must produce the same output for the same value during program execution, but may produce a different value in the next execution. #available is special because it's a checkable form of that: dynamic availability will not change while the program is running, but may be different the next time the program runs.
Given that we already intended it to be okay to change all of the return sites in new versions of a library, I can't see how this would be any worse. 
I do suggest thinking very carefully about inlinable functions, though. With those, the library author already must not change the type at all. If someone were to write a new inlinable function with an opaque result type, and rely on this rule to pick the concrete result type they want at run time, they now have to think about a set of result types that they must keep consistent. To simplify this, maybe inlinable functions should still be required to have a single result type, at least for now.