Pyright uses the following principles consistently: 1. Variable type annotations can be specified anywhere within the scope, and the location of the type annotation does not affect other aspects of type checking. x = 42 x: int # This is fine y = 42 # This should produce an error y: str 2. A variable can be annotated more than once, but the annotations need to be consistent. x: int x: int # This is fine y: int y: str # This should produce an error 3. Type narrowing is always applied within the current execution scope using code flow analysis. (The location of the variable’s type annotation does not change this.) 4. The Any type is never narrowed. “Any” indicates that the type checker should not apply any type consistency rules to that symbol, so narrowing doesn’t make sense in this case. These principles are consistent with static type checkers in other languages that I’m familiar with, and I think they are consistent with most users’ expectations. -Eric Eric Traut Microsoft Corp.