inferred type Never for unsupported in check, vs Unknown for other unsupported operators

[carljm]

I ran into this behavior today and was curious whether it is accidental, or there is reasoning behind it.

If you perform an in test with unsupported operands, pyright issues a diagnostic and infers the resulting type as Never.

For other unsupported operators, pyright infers Unknown instead.

It seems to me that in general it is correct to infer Never as the type of an expression that we are confident will raise at runtime, but in most cases type checkers seem to prefer Unknown in this situation. Perhaps this is because of a perception that Unknown will cause fewer bogus cascading errors? Although Never is usually quite forgiving as an inferred type, since it is assignable to every other type.

(FWIW, mypy infers bool for a bad membership test, which seems pretty reasonable to me as well, since Python at runtime always coerces the results of containment tests to bool. But then mypy also infers bool as the type of a bad comparison, and that seems less reasonable, since at runtime it is possible for comparison operators to give non-bool results.)

[carljm]

(Some related thoughts, not specific to pyright, at astral-sh/ruff#13932 )

[erictraut]

This specific inconsistency is accidental, not intentional.

When pyright detects a type violation of any sort, I generally try to produce a result that minimizes cascading errors, at least in "standard" type checking mode. I also try to maximize usability for users who don't care about type checking but do care about language server features like completion suggestions. Striking the right balance isn't easy in all cases. There's often no clearly "correct" answer.

As an example, consider the case where a type violation is detected on assignment. It's not clear what type should be revealed after the assignment. The "best" answer depends on which use case you're optimizing for.

x: str
x = 1  # Type violation
reveal_type(x)  # Should this be `Literal[1]`? `str`? `Unknown`? `Any`? `Never`?

These decisions get even murkier when dealing with operators such as +, which invokes either __add__ and __radd__ at runtime.

When developing pyright, I generally try to establish clear rules and principles and apply them consistently. This is one area where I wasn't as consistent as I could have been.