[Agda] Termination Checking and WIthout-K

[Joey Eremondi]

Basically, I'm wondering if there's any way to make the following file pass
the termination checker using the --without-K

https://github.com/JoeyEremondi/spire.github.io/blob/debe0a3ebbb4c82388f4f5b785b955fbc02b3d4f/source/_code/2014-08-04-inductive-recursive-descriptions/IDescIR.agda

It's a nifty combination of Descriptions and Induction-Recursion thanks to
Larry Diehl. However, if I add the --without-K flag, it complains about
foldO and foldsO not terminating.

I'm assuming this is because of the issues described here:
https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#restrictions-on-termination-checking

So I (roughly) understand the problem, but I have no idea if there's a
solution. Is this simply not a well-founded definition when K is disabled?
Or is there some trick I can use to massage this into something the
termination checker will like?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/03c34af5/attachment.html>