[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Hi Andreas,

I am now writing a merge function for trees and I've hit the same problem again.

> 1. (preferred) Avoid 'with' when possible.  In your case, there is no
> dependency in the types on (order x y), thus, use an if-then-else-like
> function instead.
This time I am using a dependently typed order:

data _≥_ : Nat → Nat → Set where
  ge0 : {y : Nat} → y ≥ zero
  geS : {x : Nat} {y : Nat} → x ≥ y → suc x ≥ suc y

data Order : Nat → Nat → Set where
  ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
  le : {x : Nat} {y : Nat} → y ≥ x → Order x y

order : (a : Nat) → (b : Nat) → Order a b
order ...

So I can't use this solution.

> 2. Use the trick to put the recursive calls into the 'with' as well.
>
>    merge (x :: xs) (y :: ys) with order x y | merge xs (y :: ys) | merge
> (x :: xs) ys
>    ... | le | call1 | call2 = call1
>    ... | ge | call1 | call2 = call2
Termination checker complains about that as well (i.e. it highlights calls to merge in the "with" 
pattern).

> 3. Define your auxiliary function yourself and in a way that lets the
> termination checker see that your call patterns are ok.
Could you point me to an example of how to do that? I'm looking at my code but I can't come up 
with a solution that would work (other than giving an explicit parameter that would limit number 
of recursive calls, but that feels wrong).

> 4. Use sized types (experimental) and --termination-depth=2.  This is
> maybe not ripe for production-use.
I'm having problems with that. I annotated my data type with {i : Size} index. Now I have merge 
function for trees (I'm eliding some details which I think are irrelevant - the code might be 
slightly inconsistent here):

merge : {i : Size} {A : Set} {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A {↑ i} (l + r)
merge .{↑ i} {A} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
          (node {i} {l1-rank} {r1-rank} l1 r1)
          (node .{i} {l2-rank} {r2-rank} l2 r2)
          = node l1 (merge r1 (node {i} l2 r2)))

and I get an error in the last line for the innermost node constructor:

  Size !=< Set of type Set when checking that the expression i has type Set

Why does it expect {i} to be Set? The definition of my data type is:

data Tree (A : Set) : {i : Size} → Nat → Set where
  empty : {i : Size} → Tree A {↑ i} zero
  node  : {i : Size} → {l r : Nat} → Tree A {i} l → Tree A {i} r → Tree A {↑ i} (suc (l + r))

Janek