>VS code = executing arbitrary python code. What stops me from deleting $HOME inside make_typed_dict?

Easy make IO calls illegal in the type checker. The type checker of course needs to execute code in a sandbox. It won't be the full python language. Idris ALREADY does this.