Totality checker issue when inductive data-type use is in a parameter of another data-type

[Termina1]

mutual
  data First = FirstSimple | FirstSecond Second
  data Second = SecondSimple | SecondFirst (List First)

mutual
  calculate : First -> Nat
  calculate FirstSimple = 1
  calculate (FirstSecond x) = calculateSecond x
    where
      calculateSecond : Second -> Nat
      calculateSecond SecondSimple = 2
      calculateSecond (SecondFirst xs) = calculateMany xs


  calculateMany : List First -> Nat
  calculateMany xs = foldl (\acc, el => (calculate el) + acc) 0 xs

Idris totality checker thinks the function calculate is not total, however if I change the last line using foldl:

mutual
  data First = FirstSimple | FirstSecond Second
  data Second = SecondSimple | SecondFirst (List First)

mutual
  calculate : First -> Nat
  calculate FirstSimple = 1
  calculate (FirstSecond x) = calculateSecond x
    where
      calculateSecond : Second -> Nat
      calculateSecond SecondSimple = 2
      calculateSecond (SecondFirst xs) = calculateMany xs


  calculateMany : List First -> Nat
  calculateMany xs = foldl (+) 0 (map calculate xs)

Idris assumes calculate is total, what's the reason. Could you explain is it a bug or expected behaviour?

[anton-trunov]

I translated the above mutual inductive definition into a type family and can confirm that the totality checker doesn't see the calculate function as total. Tested with Idris Version 0.99-git:6f46ba0e. Incidentally, Coq recognizes the function as total.

data FS : (switch : Bool) -> Type where
  FirstSimple : FS False
  FirstSecond : FS True -> FS False
  SecondSimple : FS True
  SecondFirst : List (FS False) -> FS True

calculate : FS b -> Nat
calculate FirstSimple = 1
calculate (FirstSecond x) = calculate x
calculate SecondSimple = 2
calculate (SecondFirst xs) = sum $ map calculate xs

[ahmadsalim]

Thanks for the bug report! I think I will tag this as real bug since I do not see any major reason why this should not work.

[edwinb]

It's because of the 'List' - the positivity check in Idris doesn't allow this because it only allows recursive arguments if they are either direct uses of the type, or the return type of a higher order function.

There's no reason not to allow this, it just needs implementing.

[edwinb]

Oh, and the other issue is that 'calculate' is used as an argument to a higher order function, and the totality checker can't immediately see that this is valid. This is much harder to do anything about. I don't know how Coq manages to spot that this is okay... I suppose I'll have to read up on how their totality checker works these days.