Totality doesn't check with`map`

[jiaminglu]

Idris version: 1.3.1

Steps to Reproduce

For example, I have the following code:

data Tree = Branches (List Tree) | Node Int

sumTree : Tree -> Int
sumTree (Branches xs) = sum (map sumTree xs)
sumTree (Node x) = x

If I want it pass the totality check, I have to expand map manually:

data Tree = Branches (List Tree) | Node Int

sumTree : Tree -> Int
sumTree (Branches xs) = sum' xs where
  sum' [] = 0
  sum' (x::xs) = sumTree x + sum' xs
sumTree (Node x) = x

Which makes a lot of power of functional programming not available.

Expected Behavior

The totality should check.

Observed Behavior

It's not.

[anton-trunov]

Here is an analogous Coq function that is considered total:

From Coq Require Import List.

Inductive Tree :=
  Branches : list Tree -> Tree | Node : nat -> Tree.

Definition sum (xs : list nat) := fold_right plus 0 xs.

Fixpoint sumTree (t : Tree) : nat :=
  match t with
  | Branches xs => sum (map sumTree xs)
  | Node x => x
  end.