Yes, it seems that the issue is essentially one of binding the type to a scope but then mutating within that scope. The type system could just "look" for those mutations, or the language could add mutability to the type system.

> The type system could just "look" for those mutations

That's a very big "just". Typescript and mypy don't look through function call boundaries, doing so would open a lot of problems, I believe.

> or the language could add mutability to the type system.

I agree there, the core issue is that the call to `foo` leaks a an object where the member is rebindable through assignment, but the "flow typing" assumes that doesn't happen. Ideally such a call should be a barrier for flow typing, unless there was a way to specify functions that don't modify their parameter this way (readonly parameters?).

A similar problem but with a global instead:

https://www.typescriptlang.org/play?#code/DYUwLgBAlhBcEDsCuB...

This should be handled differently. Every function should be assumed to modify globals, unless they can be marked to be pure.

Yeah, that is definitely a big "just" - it's basically whole program type inference, which I expect to be very messy in Python, if not intractable.

> unless there was a way to specify functions that don't modify their parameter this way (readonly parameters?).

Right, so in a language with typed mutability (ie: Rust) or total immutability flow typing would be a lot easier to implement without these footguns. Python is such an insane language, I'm not surprised to see that you can subvert the type checker like this.