Earlier quoted context omitted.
Dependent types are able to express the constraints that prevent or catch this error. The types of the arguments to the function can have value constraints on it, and those constraints can be determined from a value that exists there: the name of the function.
Not only do dependent types have huge decidability issues, it's my understanding that integrating them with side effects is still an area of active research.
First, I don't know that dependent types have huge decidability issues that are an inherent obstacle in general; Idris for one has a very practical and elegant model of computation – things like totality checking, linearity rules and elimination of "scaffolding" types do a lot for us.
Dependent types do allow telling the compiler about more dimensions to consider – in a way that allows for a computational explosion at compile time – but those were always an available to consider as part of the computation; Dependent types dont add that complexity, rather they allow us to address it in the type system. I see it such that we're in a stronger position to manage and navigate that complexity by allowing us to express it to the compiler in a succinct and clear way near the core context of desired action. Dependent types allow us to do less by allowing us to do more.
And integrating purely functional mechanisms with side effects is a fun and interesting avenue of research, and I don't know that adding dependent types makes that more difficult; I'd think it makes it easier?