[Agda] termination proofs

[Serge D. Mechveliani]

People, 
I have a question on the termination proofs.
Consider the example:

  merge : List Nat x List Nat -> List Nat        
  merge ([] ,      ys     ) =  ys
  merge (xs ,      []     ) =  xs
  merge (x :: xs , y :: ys)  with  x <=? y
  ...                    | yes _ =  x :: (merge (xs ,      y :: ys))
  ...                    | _     =  y :: (merge (x :: xs , ys     ))

(a couple of math symbols are replaced, for this letter).
Agda-2.3.0.1  reports  "Termination checking failed ...". 

I hoped that each the argument   (xs , y:: ys)  and  (x :: xs , ys)
is syntactically smaller than    (x :: xs , y ::ys),

that the compiler would find it, and that this is sufficient for the
termination proof.

Has it sense considering some development for the Agda termination 
syntax ordering?

What may be a possibly simple way out for this particular program?
To introduce to the loop an additional argument of  
                                       l = length (xs ++ ys)  : Nat 
?
(similarly, put  counterList = xs ++ ys,  and remove the head from  
counterList in the loop).

Now, for a general situation: my current naive idea is as follows.
(1) The programmer introduces for each problem function  foo  the size 
    function   
             size-foo : <arguments of foo> -> Nat
    and adds its value  s  to the arguments -- which makes it  foo'.
(2) The proof is provided in the program loop for that  
    size-foo args > size-foo args'  for  args  and  args'  from LHS 
    and RHS respectively ...
(3) s == 0  is set as an additional stop point for  foo' (and the proof 
    is provided in the result for the aimed properties of  foo, foo').

Seeing (1), (2), (3), the compiler will hopefully decide that  foo'
terminates, and this looks like a verification.

What an approach does  Agda  suggest for a programmer?

Thank you in advance for explanation,

-------
Sergei