[Agda] Terminating checking for functions on induction-recursion

[Jason Hu]

Hi all,

I am hitting a case where termination checker is unhappy with two mutual functions on my induction-recursion definitions. I am still trying to nail down a smaller reproduction but at least I would like to have an understanding of how things work.

Essentially I have a PER model for dependently typed languages, where I define a PER U and another PER on U:

U A B : means A and B are two values related by U. That is A and B are two types.
Given (AB : U A B), El AB a b: means a and b are two values related by El AB, where El AB computes the PER generated by the type A (or equivalently B).

Now I shall move on to prove symmetry. I have

​mutual
  U-sym : U A B -> U B A
  U-sym AB = ...

  El-sym : (AB : U A B) (BA : U B A) -> El AB a b -> El BA b a
  El-sym AB BA = ...

Now,  U-sym  proceeds by pattern matching on AB and El-sym proceeds by pattern matching on AB and BA. In U-sym, I can call U-sym and El-sym on smaller structure. However, for some reason, in El-sym, I can only El-sym on smaller structure. Any call of U-sym on smaller structure in El-sym will  (almost) cause a termination checking error*.

I cannot possibly figure out why calling U-sym in El-sym is forbidden. How exactly termination checking with induction-recursion definitions work in Agda? Could anyone give some insights about what could go wrong if U-sym can be called in El-sym, if Agda is doing the right thing?

* almost means I have counterexample but I cannot summarize the pattern

Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211109/48b14d33/attachment.html>