[Agda] successor / predecessor definition rejected for a tree-based natural number type

[Paul Tarau]

{-
The following successor / predecessor definition
for a tree-based natural number data type is
rejected by Agda 2.3.2.1 with:

Not in scope:
  x at /Users/tarau/Desktop/go/art/lit/coq/vw.agda:24,27-28
when scope checking x
-}

module VW where
open import Data.List

data T : Set where
  E : T
  V : T -> List T -> T
  W : T -> List T -> T

mutual

  s : T -> T  
  s E = V E []
  s (V E []) =  W E []
  s (V E (x::xs)) =  W (s x) xs  {- agda error here, claims x not in scope -}
  s (V z xs) = W E (s' z :: xs)
  s (W z [])  = V (s z) []
  s (W z [E]) = V z [E]
  s (W z (E::y::ys)) = V z (s y::ys)
  s (W z (x::xs)) = V z (E::s' x::xs)

  s' : T -> T 
  s' (V E []) = E
  s' (V z []) = W (s' z) []
  s' (V z [E]) =  W z [E]
  s' (V z (E::x::xs)) =  W z (s x::xs)  
  s' (V z (x::xs)) =  W z (E::s' x::xs)  
  s' (W E []) = V E []
  s' (W E (x::xs)) = V (s x) xs 
  s' (W z xs) = V E (s' z::xs)

{-
Its (attached) Coq equivalent passes termination check,
and while the recursion is mutual, calls are
only made on structurally smaller arguments.

Is this a limitation of Agda's termination checker,
something related to using x inside a list construct
or something else that I am missing? 

Thanks in advance for any hints on what's going on,

Paul

P.S. I am just 1-day new to Agda but I am planning to
splash in more deeply, as it is syntactically  quite
friendly to my existing Haskell code at

http://logic.cse.unt.edu/tarau/Research/2013/hbin.hs

for which I want to prove equivalence with (the Peano 
algebra of) natural numbers. The complete story is 
explained in detail at

http://logic.cse.unt.edu/tarau/Research/2013/hbin.pdf

and some of the applications are at

http://logic.cse.unt.edu/tarau/Research/2013/hbs.pdf
-}


{- same in Coq - passes termination check

Require Import List.

Inductive T : Type :=
| E : T
| V : T -> list T -> T
| W : T -> list T -> T.

Fixpoint s (t:T) :=
match t with
| E => V E nil
| V E nil =>  W E nil
| V E (x::xs) =>  W (s x) xs 
| V z xs => W E (s' z :: xs)
| W z nil => V (s z) nil
| W z (E::nil) => V z (E::nil)
| W z (E::y::ys) => V z (s y::ys)
| W z (x::xs) => V z (E::s' x::xs)
end 
with 
s' (t:T) : T :=
match t with
| V E nil => E
| V z nil => W (s' z) nil
| V z (E::nil) =>  W z (E::nil)
| V z (E::x::xs) =>  W z (s x::xs)  
| V z (x::xs) =>  W z (E::s' x::xs) 
| W E nil => V E nil
| W E (x::xs) => V (s x) xs 
| W z xs => V E (s' z::xs)
| E => E (* pro forma *)
end.
-}