[Agda] Termination

[Geoffrey Alan Washburn]

I've just encountered my first problem with termination.  Here is a 
really simplified example of the problem:

   Test where
   open import Data.List
   open import Data.Nat

   data Tree : Set where
     Leaf : ℕ -> Tree
     Node : [ Tree ] -> Tree

   inc : Tree -> Tree
   inc (Leaf n) = Leaf (n + 1)
   inc (Node ts) = Node (Data.List.map inc ts)

Essentially, it seems that Agda cannot tell that passing inc to map will 
be terminating.  It does not seem to be an issue of modularity 
preventing unwinding, as I can define my own list data type and map in 
the same file and it still flags it as non-terminating.

This kind of recursion is not a problem for Coq's termination checker, 
at least as long as you've defined map properly, so is there something I 
am just doing incorrectly here?  Or is the only solution here to define 
a specialized version of map mutually recursively with inc?