Should narrowing be applied on initial assignment?

[KotlinIsland]

o: object = 1
reveal_type(o)  # object or 1?

It can be frustrating is certain circumstances:

a: object = 1
print(a + 1)  # error: Unsupported operand types for + ("object" and "int")

a = "amoogus"
print(a + "SUS")

And forces you to write code that you normally wouldn't:

a: object 
a = 1
print(a + 1)  # no error: mypy happy now 😀

a = "amoogus"
print(a + "SUS")

counterpoint:

i know typescript behaves that way however i'm not really a fan of that behavior, i think the explicit type annotation should widen it, for the same reason that i wouldn't expect this to be narrowed just because of the return value:

def foo() -> int | None:
   return 1

- @DetachHead

I guess the question is: should the explicit type annotation act like a cast, or an upper bound?

[DetachHead]

here's a better example of when this behavior is annoying in typescript. when i explicitly specify the type as being wider, the compiler shouldn't ignore me:

let foo: boolean = false

const changeFoo = () => {
    foo = true
}

declare const condition: boolean

if (condition) {
    changeFoo()
}

if (foo) {
    foo //never
}

playground

perhaps it could be argued that it should behave like this for Final variables, but i don't really see the point

[KotlinIsland]

This seems more like the more general case of mutation after narrowing:

def mutate():
    global a
    a = ""

a: object

if isinstance(a, int):
   mutate()
   print(a + 1)