@MartinEscardo I commiserate, but somewhat unfortunately "make termination more accepting of [X syntactic transformation]" tends to devolve into "make termination more accepting of ⊥", like the old with-inlining transformation. There was some dead code in the termination checker for "matrix-shaped orders", which would allow componentwise comparison of record values against record patterns, but, well, it was never finished, so we just axed it.

I'm planning to fix our documentation to call out cases like this, but there's so much to fix with the documentation that I'm stuck figuring out where to even start. For now I would offer the informal heuristic that "recursive calls must be made 'on' top-level arguments to the function, whose types can be seen to be inductive from the function's signature."

@de_Jong_Tom @totbwf