[@overload]: What is the effect of the *implementation* type-signature?

One thing that I've found underspecified when using @overload is what the type signature of the actual function should be.

For example, let's say I have a function like:

from typing import overload, Literal

@overload
def f(x: int, z: Literal[True]) -> str: ...
@overload
def f(x: int, z: Literal[False] = ...) -> int: ...
def f(x: int, z: bool = False) -> str | int:
    if z:
        return "hello"
    return 1

What is the effect of the last line? In particular:

• The documentation and examples often just use no annotations for the implementation signature (def f(x, z):). Is that the right thing to do (I sometimes get Overloaded implementation is not consistent with signature of overload 1 errors if I leave out the type annotations)?
• If I do specify types on the last, do I also have to add it to @overload list -- in other words:

@overload
def f(x: int, z: Literal[True]) -> str: ...
@overload
def f(x: int, z: Literal[False] = ...) -> int: ...
@overload
def f(x: int, z: bool = ...) -> str | int   # is this overload necessary?
def f(x: int, z: bool = False) -> str | int:
    if z:
        return "hello"
    return 1

Both pyright and mypy seem to interpret things differently with and without it (e.g. see this play link).

I understand that @overload is a complicated feature, but I'm hoping this is a small corner we can start with.

Start with the @overload examples in this issue and run them in the linked Pyright playground, then compare the results with mypy. Review how the two tools interpret implementation signatures and overload lists. Done means reaching an agreed explanation of the semantics and documenting the expected behavior and examples.