I found Jukka’s referenced comment to be valuable, so here’s a direct link:
https://github.com/python/mypy/issues/2008#issuecomment-296213676 Eg, I believe pyright’s narrowing to Animal corresponds in part to Jukka’s Proposal 2 (or Proposal 4), which he mentions is TypeScript’s behaviour: when narrowing a Union, narrow to a member of the Union.
My view on the invariance issue is the most natural flow is to start with:
```
def g(x: Foo[Union[int, str]]): ...
def f() -> None:
y = 1
a = Foo(y)
g(a)
```
Then get an error (with a very clear message / suggestion) and add:
```
def f() -> None:
y = 1
a: Foo[Union[int, str]] = Foo(y)
g(a)
```
Which is fine in the presence of type narrowing, because obviously we shouldn’t narrow to an incompatible type. (It’s also my opinion that this is the type annotation that best helps describe what’s happening)
I don’t know that I’d be so quick to write off always narrowing (modulo Any), which I believe corresponds to Jukka’s Proposal 3. I’d be curious to know more about the significant number of false positives you’d expect; that seems contra my intuition and the results on the sample corpus Jukka described. It also feels wrong to mandate that all future type checkers can’t narrow in part because a majority of our current ones do not. It feels like if a type checker can prove something about a value, it should be fair game (and that as long as users can see that proof is possible, we’ll get bug reports).
Generally speaking, it’s surprising to me to make a usability argument for a distinction that most end users wouldn’t notice or weren’t making with intention. But maybe this is a case where if the behaviour is PEP-ed users will no longer find it surprising.