I’ll share a proposal within a week or so that will address some (though not all) of your points, creating a path towards a specification.
Overall, your list of issues looks diverse, and not all issues can be addressed by this group. (For example, we don’t have control over how VSCode does autocomplete.)
The biggest disconnect is probably around soundness. You clearly care deeply about making the type system sound, but for many type checkers full soundness has not historically been a goal. And for type checkers like mypy and pyright that are used by numerous projects, any changes now can have backward compatibility considerations, so even if the maintainers of these type checkers agree with soundness as a goal (they may not!), it will take them a long time to get there.