Pretty sure it's impossible to allow IO without enabling all of it one way or another. And as soon as you allow *any* IO, you're open to various kinds of failures including segfaults. The only way you will get your type system to prevent that is fully specified dependent typing both in your program *and in the OS level interfaces*. I wish you luck on the latter.

I don't agree.  This would seem to imply that type safe / memory safe imperative languages are impossible, and that OCaml/Java/C#/etc are a false promise!

Which APIs and dangers are you thinking of?  I'm worried about bounds checks on memory access, and the capability of foreign code to poke at arbitrary memory.

But other APIs like these should be fine:
  • IORef API
  • MVar API
  • STM API
  • File IO API