conformance: Fix TypeIs Any intersection case#2236
conformance: Fix TypeIs Any intersection case#2236JelleZijlstra wants to merge 1 commit intopython:mainfrom
Conversation
The `assert_type(val, int)` here is incorrect in the negative case if a type checker is sufficiently precise in its implementation of intersections. ty currently infers int & ~Awaitable[object], apparently because it has chosen to always use the top materialization of TypeIs. A change I am about to make to pycroscope will have it infer `int | Awaitable[int]`, because it drops the negated part of Not types.
| # (int | Awaitable[int]) & ~Awaitable[Any], but conformant implementations | ||
| # may simplify this. | ||
| # But it should definitely remain assignable to `int | Awaitable[int]`. | ||
| y: int | Awaitable[int] = val |
There was a problem hiding this comment.
I feel like this isn't testing all that much anymore. Not sure how to improve it, though ^^;
There was a problem hiding this comment.
Yes, unfortunately I can't think of a better way here. Using theoretically correct intersection semantics is not always practical. For reference here are the tests I added to pycroscope while looking at this: https://github.com/JelleZijlstra/pycroscope/pull/444/changes#diff-17d47f7718e5c338fb6076c1e2971a2ca798555e661e881cd1653cf5e54d99fe
I tried both TypeIs[Awaitable[Any]] and TypeIs[Awaitable[object]].
Among the current type checkers, two type checkers actually have explicit intersections, but neither produces the full theoretically correct types. Ty treats the Awaitable[Any] TypeIs as if it's Awaitable[object]. That behaves better in some cases but worse in others; in this check it means that y: int = await val is rejected because val might also be int & Awaitable[object]. Pycroscope (unreleased version) doesn't do that but it drops negation types, so the else branch types are simpler.
Three of the other type checkers (mypy, zuban, pyright) narrow to Awaitable[int] and int for both the Any and object guards; pyrefly narrows to Awaitable[Any] for the TypeIs[Awaitable[Any]]. This is unsound but perhaps more practical than the precise intersection behavior.
3 participants
The
assert_type(val, int)here is incorrect in the negative caseif a type checker is sufficiently precise in its implementation of
intersections.
ty currently infers int & ~Awaitable[object], apparently because it
has chosen to always use the top materialization of TypeIs. A change
I am about to make to pycroscope will have it infer
int | Awaitable[int],because it drops the negated part of Not types.