I have a few thoughts.
The proposed spec change in Clarifying the float/int/complex special case - #19 should in fact make it easier to spell the “float but not int” type, because that spec change makes it clear that the float/int special case applies only at the syntactic level; it is not a special case in the subtyping rules. If this proposal is accepted and if difference types are added to the type system, then float - int (or float & ~int) would in fact be a viable way to spell “float but not int”.
I was curious about the impact of this idea, so the other day I made a draft change to mypy to remove the special case: Experiment: Remove int/float promotion by JelleZijlstra · Pull Request #17279 · python/mypy · GitHub. The mypy-primer tool, which runs on mypy PRs, tells us about any changes in type checker output caused by this change in various open source projects. Unsurprisingly, the impact is huge: over a thousand lines of new errors across the mypy-primer corpus. I was able to reduce those by about half by codemodding : float to : float | int across the standard library in typeshed. (That’s a less sophisticated version of the migration tools that some previous posts suggested; my codemod wouldn’t have changed a parameter annotation like x: str | float.)
Part of why we have this special case is that the Python standard library takes pains to always supports ints where floats are supported. The argument parsing APIs for accepting floats in C code all also accept ints. Therefore, it is really very rare (though not impossible) for a function to accept only float but not int. The proposed option 1 would imply that virtually every parameter annotation float in Python type would have to be changed to float | int.
I don’t have the stomach for such a disruptive change. I would prefer to change the spec now to make it clear that this special case applies only at the syntactic level, and then wait for difference types to be added so that we have a way to spell “float but not int”.