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.
Right. I am trying to brighten that line between the sophistication of type systems, the runtime performance of programs and the simplicity of code. I think they are connected in interesting ways, and some of the more rewarding learning I've ever done has consisted of using more sophisticated type system techniques without paying too much on the performance and/or simplicity side of things.
