[Agda] Termination checking in cubical mode

[Dr. ERDI Gergo]

I realized that my code was missing one crucial detail: I didn't 
explicitly add truncation of paths to my datatype. With that change, I was 
able to write `right` without any recursive reference, which in turn 
allowed my whole program to typecheck. My full working code is at 
https://stackoverflow.com/a/53246786/477476

I did run into some problems when trying to write the binary function _+_ 
using pattern matching (weird errors about "function is not fibrant"), so 
I ended up defining an explicit eliminator for my HIT and using that; I 
can try to make a small self-contained example showing the problem if it 
is interesting (maybe it's just another example of 
https://github.com/agda/agda/issues/3314)


On Fri, 9 Nov 2018, Dr. ERDI Gergo wrote:

> 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