Dependent types are cool, but I think the best fix would be refinement types. They are sort of similar, except refinement types use a SAT solver to prove correctness, while dependent types require to prove everything yourself (to the point where realistically something like what you posted probably wouldn't compile in most dependently typed languages). Refinement types also compose better.

Because of the SAT solver you have some restrictions on what you can prove, but they're so much more ergonomic I think it's more than worth it.