[Agda] Termination checking in cubical mode

[Dr. ERDI Gergo]

Hi,

I've played around with Agda's --cubical mode, using 
https://github.com/agda/cubical (after being pointed to it on Stack 
Overflow). My current code typechecks, but trips up the termiation 
checker in the definition of a binary function over HITs.

1. The code that I initially wrote is here: 
https://gist.github.com/gergoerdi/f8e7d20fc45ee0f6dba52161df2c59c4

In this version, the termination checker complains about basically every 
occurrence of `_+_` in the internal point case (i.e. the fourth clause). I 
don't think this behaviour is justified: all the corner and edge cases[1] 
are covered by the previous three clauses of `_+_` which have no recursive 
calls.

Is there any valid reason why these `point + point` etc. cases are 
reported as "problematic", or is this just an implementation shortcoming?


2. If I inline the definition of `_+_` in `X + A` etc. as in
     X+A = (x +̂ a) - (y +̂ b)

then the only remaining problematic calls are the ones in the definition 
of `right`:

     right : qᵢ i1 ≡ q₁
     right i = comp
       (λ j → p j + A ≡ p j + A′)
       (λ { j (i = i0) → qᵢ j
          ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
          })
       (inc (left i))

Here, again, the `p j + A` and the `p j + A′` case should be covered by 
previous clauses (since both are on edges). But the `_+_` in the `cong` 
call looks like a valid problem.

Supposing that all the other problems are resolved (either by fixing 
some bug in Agda's termination checker, or me manually inlining all 
corner- and edge-calls of `_+_`[2]), what is the general strategy for 
referring to the function being defined, when defining functions over 
HITs, without causing termination problems? In other words, what can I do 
with this last remaining `_+_` call in `cong`

FWIW, since my HIT is a quotient type, I think morally just defining it on 
the corners and edges should be sufficient, so no "real" information is 
being added in the inner point case.

Thanks,
 	Gergo


[1] I love how 'corner case' and 'edge case' are actual technical terms in 
CTT!

[2] I guess the latter is going to happen faster