What's the rationale behind ["the first explicit argument maps to the second parameter"]?
Without this, it would be impossible to implement a user-defined type guard function as a method. If you want to apply a type guard to self, you can pass `self` as the first argument, which maps to the first explicit parameter.
What's the rationale for user-defined type guards to only apply in the positive case?
The problem is that `T - guarded_type` is not well defined in the general case. This sort of type algebra is defined only in very specific cases (such as with unions). In general, the negative case must assume no narrowing. For comparison, this is how user-defined type guards work in TypeScript, by necessity.
Can you think of an example of a user-defined type guard (one that is not handled by built-in type guards) that could handle the negative case? None of the examples I provided in the draft PEP would work.
Incidentally, I've posted more detailed documentation for the [type narrowing behaviors and all of the built-in type guards that pyright supports](https://github.com/microsoft/pyright/blob/master/docs/type-concepts.md#type-...).