I did some more research about this, and re-read Jukka's big comment in the thread I mentioned. I also chatted to Jukka off-line, and he suggested we come up with a PEP. Finally, I tabulated the status quo across the four type checkers and 5 different examples.

It seems pyright is the big outlier here -- its philosophy appears to be inspired by choices made in TypeScript, while everyone else has tried to follow mypy's guidance or tried to maximize usability for a large existing code base. The latter is actually also the inspiration for mypy's choices, hence the tendency towards alignment.

The key question is whether there's a difference between the following two fragments:
```
# (1)
a: T = x

# (2)
a: T
a = x
```
Here T is a type, and x is a value of a *subtype* of T, let's call that U.

The question is, when `a` is then used in an expression, does it behave like its type is T or U. IOW does it narrow (to U) or not?

(Aside: all checkers remember a's original type T even if they narrow, and allow assignments from other subtypes of T. This is as it should be.)

Pyright, unique among type checkers, treats the two forms the same regardless of what kind of thing T is. The other three, with one or two exceptions, treat form (1) as a "gentle cast", keeping the wider type T as the type of `a`, while they treat the assignment in form (2) as an opportunity to "implicitly narrow" the type.

The first exception is a special case if T is Any. Taking Rebecca's word that what I observed in pytype is a bug, everyone except pyre makes an exception so that if T is Any, form (2) doesn't narrow. Even pyright takes this stance. Interestingly, pyre *always* narrows in this case. I propose that pyre changes, since it's useful to be able to say `a: Any` to prevent any type checking involving `a`. It seems Shannon agrees.

The other exception is that there seem to be different behaviors for the case where T is some Union compared to the case where T is a base class of U. I didn't show this in my OP, so here's some sample code:
```
class Animal: ...
class Bear(Animal): ...

def s1() -> Bear:
    a: Animal = Bear()
    return a  # Animal, except Animal in pyre
   
def s2() -> Bear:
    a: Animal
    a = Bear()
    return a  # Bear, except Animal in pyright
```
Most checkers keep Animal as the type in the first example, and narrow to Bear in the second example.

Pyre is an exception here and assumes the type Bear in both cases. In contrast, pyright assumes Animal in both cases.

If we combine this with the Union example, we get even more interesting behavior:
```
def t1() -> Bear:
    a: Union[Animal, int] = Bear()
    return a  # Union[Animal, int], except Animal in pyright

def t2() -> Bear:
    a: Union[Animal, int]
    a = Bear()
    return a  # Bear, except Animal in pyright
```

I will now try to make sense of this mess.

First, I am sorry to say that pyright isn't right. :-) There *should* be a difference between form (1), "gentle cast", and form (2), "implicit narrowing". This is a matter of usability -- for (1), the user explicitly says "this is a T" and the checker should respect that, while for (2), the user says "I am assigning this U to that T" and the type checker should treat the variable as a U. This is all subject to flow control; e.g. we can write
```
def f(a: T):
    # here it's a T
    if foo():
        a = x  # of type U
        # here it's a U
    # here it's a T again
Second, pyright violates animal rights. :-) Everyone else narrows from Animal to Bear (at least in form (2)), but pyright doesn't. When T is `Union[Animal, int]` and U is Bear, the narrowed form is Animal. I don't understand what guiding principle applies here.

Third, I think there should be a special case for Any -- when T is Any, no narrowing should happen. Pyre is in the wrong here for both form (1) and form (2). (Pytype also appears in the wrong for form (2) but Rebecca says this is an unrelated bug.)

Fourth, Shannon seems to think that it's a Pyre bug that form (1) and form (2) aren't treated the same if T is a Union. Here I plead, please keep this behavior, I think it's the most useful.

Finally, several end users have expressed their surprise that there ever is a difference between form (1) and form (2). They are not alone -- the mypy tracker shows that this requires some explaining, and PEP 526 claims there is no difference. But I've been convinced that it's the right thing to make this distinction. The alternative would be to *always* narrow (perhaps with an exception for Any) but that would require a majority of checkers to change, which sounds like inflicting unnecessary pain. In the mypy tracker you can find hints that doing this would cause a significant number of false positives in a large real-world code base to which I no longer have access.

--
--Guido van Rossum (python.org/~guido)
Pronouns: he/him (why is my pronoun here?)