Well, the point isn't to have errors for a lack of documentation, the point is that dependent types offer a lot of expressiveness in modelling what it means for

Well, the point isn't to have errors for a lack of documentation, the point is that dependent types offer a lot of expressiveness in modelling what it means for programs to be valid in your domain, both so the compiler can tell the programmer about subtleties they may have missed, and the programmer knows what details of the implementation are intentional features (e.g. every case this function handles has a corresponding entry in a table of documentation).