[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

> Ulf recently changed Agda to reduce the need for workarounds:
>
>    Issue 59: Improving termination checking of functions defined using
>              with
>    http://code.google.com/p/agda/issues/detail?id=59
>
> You may want to try the latest development version.
I just installed the latest version from repository and indeed there are improvements. Agda no 
longer complains about:

merge : List Nat → List Nat → List Nat
merge nil       ys             = ys
merge xs        nil            = xs
merge (x :: xs) (y :: ys) with order x y
merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)
merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys

but it still complains about this:

mergeO : {b : Nat} → OList b → OList b → OList b
mergeO onil ys = ys
mergeO (ocons x blex xs) onil = ocons x blex xs
mergeO (ocons x blex xs) (ocons y bley ys) with orderD x y
mergeO (ocons x blex xs) (ocons y bley ys) | le xley =
  ocons x blex (mergeO xs (ocons y xley ys))
mergeO (ocons x blex xs) (ocons y bley ys) | ge ylex =
  ocons y bley (mergeO (ocons x ylex xs) ys)

I presume the reason is that parameter to recursive call is not an exact reconstruction of the 
input parameter (notice how bley is replaced by xley or blex by ylex). Idris is smarter here and 
correctly detects that mergeO is total.

Janek