Mutation invariably involves....invariance. There are many ways of looking at this, here is mine: If a := b and a.F := c, then we must assume b.F := c is possible. However, such edges are not tractable in a type system, so we conservatively rely on invariance instead.
Agreed. (Syntactic) types are exactly incoherent with the kind of "spooky action at a distance" that mutability enables. Semantic type layers could do more, perhaps.
I've got a whole type system going based on non-syntactic types that supports aggressive type inference in the presence of subtyping. It uses type trees rather than coercions, and types are built based on observation. Will write more aboit it soon.
