Some more follow up :-)
First, I attached a file that contains six functions we care about and the behaviours of the four checkers + some of Jukka's proposals (previously linked). This assumes that things are subject to flow control and that checkers allow reassignments based on the declared type. I was going a little cross eyed, hopefully it helps clarify the state of things. (Apologies if I got something wrong!)
Next, the question was brought up as to why TypeScript behaves the way it does. I’m not particularly familiar with TypeScript, so I can’t claim to know for sure, but I did some digging:
tldr; I'm not convinced there's a good reason. It seems like they just went from always using the annotation to always using the annotation except for unions in order to have a better null story.
It looks like they implemented flow based narrowing in 2016, notably narrowing for unions:
Shortly after, they receive a complaint and discuss other narrowing. The variance narrowing issue gets brought up (along with optional properties, which I think don't matter to us):
It’s then mentioned as a thing they’re still talking about. But null is a reason for wanting to have something in place for unions:
It seems to still get brought up from time to time:
It's also worth asking why mypy currently doesn't abide by PEP 526. It's possible this is just a quirk of history, stemming from the evolution of type comments. mypy's behaviour appears to be the same as Proposal 4, except for not narrowing unions. I think that’s why Proposal 4 exists: it’s the most conservative change for mypy that would help with the original issue report in issue #2008.
Finally, some discussion of arguments against narrowing. Naturally these apply most to Proposal 3, which always narrows, but they do also apply to various status quos. These arguments are presented in Jukka's cons of Proposal 3 (I'd be curious if other arguments surface).
As discussed previously, I’m not fazed by the invariance argument (assuming you narrow to a compatible type).
I think I’ve also made my peace with the Sequence / disallowing local mutability argument, since it seems a little too treacherous to be relied on / you can always be explicit and cast / maybe use Final. I’d also want to see usage in real world code here.
I do think the interactions with Any are something that need some thought. However, if there isn’t a particularly easy way of doing things cleverly, I’m not that worried about inconsistency. People use Any to stop type checkers from trying to be too clever, so preserving the current behaviour of listening to the user in the presence of Any seems fine. I think users who would complain about not narrowing in the presence of Any would also complain about not narrowing at other times.