[Agda] Termination problems with "with" and recursion

[Jan Stolarek]

Thanks for reply Jesper. Perhaps I ommitied something important when trying to simplify my 
example. Full code is below:

========== START CODE ==========

module MergeSort where

record Sg (S : Set)(T : S → Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public
_×_ : Set → Set → Set
S × T = Sg S λ _ → T
infixr 4 _,_ _×_

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Order : Set where
  le ge : Order

data List (X : Set) : Set where
  nil  : List X
  _::_ : X → List X → List X

order : Nat → Nat → Order
order zero    y       = le
order (suc x) zero    = ge
order (suc x) (suc y) = order x y

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

deal : {X : Set} → List X → List X × List X
deal nil        = nil , nil
deal (x :: nil) = x :: nil , nil
deal (y :: (z :: xs)) with deal xs
deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs

sort : List Nat → List Nat
sort xs with deal xs
sort xs | ys , nil = ys
sort xs | ys , zs  = merge (sort ys) (sort zs)

========== END CODE ==========

I have problems with merge and sort.

Janek