As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types.

   How does that fit

Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is complicated and correctness so important that testing is insufficient, then I recommend post-programming verification with a program logic.