Maybe the typical "pedestrian" problems, like lists having non-zero length, or numbers being in a given range, can be checked statically with simpler means that full-on dependent types?

E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.