I also don't see them handling imperative mutations that expand/change a variable's type at that "temporal location" for so long until it is next mutated elsewhere
Locally if all cases of mutation agree in typestate then the type transitions can be inferred, e.g. the same type transforms occur in either branch of an if