I didn't delve too deeply, but I don't get it. How do you get provable runtime safety (in a dependent types sense) in a system which gives you direct control over memory, and without introducing the kind of overhead that would be inappropriate for a systems language?

Your "overflow, then inspect" example illustrates this incoherency. If overflow is allowed, and you try to fit 250 + 10 into a u8, so the value should be 4, which is less than 10, so it should fit your precondition, not violate it. And this is a simple example where 250+10 is known at compile-time - what happens when a user provides the number at run-time? Does the compiler attempt to provide the proof anyway? How?

I mean.... I have a lot of respect for Haskell and Idris and the goals they set out. But they're not systems languages.