I think you are referring to concrete/mainstream languages - so what you are writing is correct from a practical perspective, i.e. I would do that. From a theoretical perspective however it is not necessary, even if such a type-system might not exist yet.
You can retreat to your corner of theory if you wish, I'll actually build stuff. The real world has scary things like malicious actors that will send payloads designed to break your system through side channels like timing and cosmic rays that can flip bits on your disk and erase the guarantees that you believed you had in your type system.
