[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

[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)

Post by 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.
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 : 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