Most index manipulation is fairly simple. For instance, if the result of `str.find(pat)` is `Some(pos)`, then you know that:

(0) `pos <= str.len()`.

(1) `pos` is actually the beginning of a character - it makes sense to split the string at the position `pos`.

These things are easy to check - there is not even any multiplication involved! - but a conventional type checker won't do. Much of the pain of using dependent types is the result of sticking to unification as the only basis for type-checking.