Comment by dnautics

I think this is wrong. Type systems should be simpler, and you should design it so that your language is easily and correctly statically checked. Not all invariants necessarily have to be verified at the same cadence (compile time)