Прекращение структурной индукции

Я не могу заставить программу проверки завершения Agda принимать функции, определенные с помощью структурной индукции.

Я создал следующий, как мне кажется, простейший пример, демонстрирующий эту проблему. Следующее определение размера отклоняется, хотя оно всегда рекурсивно выполняется на строго меньших компонентах.

module Tree where

open import Data.Nat
open import Data.List

data Tree : Set where
  leaf : Tree
  branch : (ts : List Tree) → Tree

size : Tree → ℕ
size leaf = 1
size (branch ts) = suc (sum (map size ts))

Есть ли общее решение этой проблемы? Нужно ли мне создавать Рекурсор для моего типа данных? Если да, как мне это сделать? (Думаю, есть пример того, как определить Рекурсор для Списка A , это даст мне достаточно подсказок?)