Shared via mypy Playground

main.py

from typing import Never

def very_sound_function() -> float:
    y: list[Never] = []
    return next(iter(y)).startswith("xyz")  # type checker approved!
    #      ^^^^^^^^^^^^^ this may have been a good place to error
    #                    if we really believed Never was uninhabited.

def make_never() -> Never:
    while True:
        pass

x: Never = make_never()  # yep, totally uninhabited.