This proposal (and variants you raised in the typing issue, like <https://github.com/python/typing/issues/996#issuecomment-1001979242>) all rely on the typeguard function knowing the precise set of types that will be passed to it in the first place, and that type union being relatively small so that the `else` type is also useful to work on. I don't think this is very useful in practice: (1) it doesn't match how existing type-checking functions often work, and (2) doesn't match the behavior of type-checking inline in your `if` condition. Instead, I think for this to be useful, false TypeGuards (or some variant of TypeGuard, to avoid changing current behavior) need to operate on *value* unions, rather than *argument* unions. 1) The existing type-narrowing checks (isinstance(), issubclass(), callable()) all (effectively?) take Any as their input type; if they return False, the type of the output is just Any minus whatever they checked for. My own typeguards in my code do the same, precisely because I might be taking any of a number of values. Since we don't have subtraction types, these functions *can't* explicitly write out their false type. In general, I don't think it's reasonable to expect type-guarding functions to have a non-Any input type at all (or at least a sufficiently narrow type union that the subtraction gives a useful type); their whole point is discriminating the one type you care about from anything else -- sometimes I'm filtering Element nodes from Comment nodes, other times from strs, other times from Nones. 2) The existing type-narrowing checks operate on *value* types, not argument types; if I have a value of type `str | Element` and I write `if isinstance(x, Element)`, the `else` branch will have narrowed x's type to `str` for me. If x's type was `str | Element | None`, the else branch will narrow to just `str | None`. The type-narrowing examples all explicitly call this behavior out. But if I move my `isinstance()` check to a type-guarding function, I lose this behavior and have to manually narrow my types in the `else`. This is the *precise* behavior that I want to maintain, however! For the sake of being productive, I suggest a variant called `TotalTypeGuard[type]`, which implies that your type-guarding function returns True for *all* values of the specified type. (Not just potentially for some, as Guido points out can happen with the current TypeGuard.) The behavior when it's false is then identical to existing built-in type-narrowers: if the value's type is a union, the specified type is removed from that union.