I think we should try to get PEP 604 accepted, with the runtime option (a), since that's the way we've gone already.
PEP 604 proposes the right syntax, and I think mostly the right semantics (one could quibble about whether isinstance()/issubclass() ought to accept unions). Unfortunately it does not have a reasonable reference implementation. (The mypy patch looks okay, but the CPython patch is not realistic, since it attempts to import typing.py from the C code for |.)
There is another PEP, PEP 585, which is complete (in fact, we should just submit it to the SC for review!). There is also a basically complete implementation, in C. It introduces a C type types.GenericAlias (note: types, not typing!) which is used to represent generics involving builtins at runtime, e.g. after "a = list[int]", a.__origin__ points to 'list' and a.__args__ is the tuple (int,).
Here's an idea for an implementation of `a | b` based on that. A union could be an instance of types.GenericAlias whose __args__ is (a, b) and whose __origin__ points to some dummy type (implemented in C) that's only used to mark it as a union.