If an async function returns Never (Awaitable[Never]), we could ideally also detect that and consider code that comes after it unreachable.

In the following example, this means we could reveal Literal[2]:

from typing import NoReturn, reveal_type

async def exit() -> NoReturn:
    raise NotImplementedError

async def main(flag):
    if flag:
        x = 1
        await exit()
    else:
        x = 2
        pass
    
    reveal_type(x)  # currently Literal[1, 2], could ideally be Literal[2]

Pyright supports this. I'm not sure if this comes up in practice. It does not seem particularly important.