> Leftpad is an entirely pure, non-diverging function. And I should be able to ask my language to enforce that, ideally with trivial code. Maybe even by default.

I think you can do this in Idris with "total" functions.