Certainly not with our existing type systems. It might be possible if somebody could come up with a new system with the vau calculus at its core rather than lam

Certainly not with our existing type systems. It might be possible if somebody could come up with a new system with the vau calculus at its core rather than lambda calculus (as Hindley-Milner etc. are). I think it would be a dead-end with kernel-standard though. The presence of mutability and cyclic data structures seems like the problem would be as unsolvable as the halting problem. For any serious investigation of type inference, you would probably need to stick to an immutable Kernel subset. The Kernel Report does make mutability optional.