Is this recursive function not total, or is the compiler just unable to prove it? How to rewrite it as total?

Question

When presented with the following code:

module TotalityOrWhat

%default total

data Instruction = Jump Nat | Return Char | Error

parse : List Char -> Instruction
parse ('j' :: '1' :: _) = Jump 1
parse ('j' :: '2' :: _) = Jump 2
parse ('j' :: '3' :: _) = Jump 3
parse ('r' :: x :: _) = Return x
parse _ = Error

parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' xs =
    case parse xs of
      (Jump j) => parseDriver' $ drop j xs
      (Return x) => Just x
      Error => Nothing

Idris gives an error:

TotalityOrWhat.idr:17:3:
TotalityOrWhat.parseDriver, parseDriver' is possibly not total due to recursive path
TotalityOrWhat.parseDriver, parseDriver' --> TotalityOrWhat.parseDriver, parseDriver'

TotalityOrWhat.idr:15:1:
TotalityOrWhat.parseDriver is possibly not total due to:
TotalityOrWhat.parseDriver, parseDriver'

I have re-written this code in several other ways but cannot get Idris to recognize it as total. Am I wrong about it being total, or is Idris just not able to determine that it is? If it is total in essence, how can I rewrite it so Idris will recognize it as total?

Answer 1

This is not an answer to "why isn't it recognized as total" and not even really an answer to "how do I change it to be recognized as total", but since you mentioned

I have re-written this code in several other ways but cannot get Idris to recognize it as total,

I thought you might be interested in a workaround. If you manually inline parse into parseDriver', you can get it through the totality checker:

total parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' ('j' :: '1' :: xs) = parseDriver' ('1' :: xs)
  parseDriver' ('j' :: '2' :: xs) = parseDriver' xs
  parseDriver' ('j' :: '3' :: _ :: xs) = parseDriver' xs
  parseDriver' ('r' :: x :: _) = Just x
  parseDriver' _ = Nothing

This works because we are always recursing structurally on some suffix of xs.

Answer 2

The problem here is that Idris can't know that drop j xs produces a strictly smaller list from its input, since drop's type isn't expressive enough.

So, another ad-hoc approach would be to use a dummy parameter which makes the totality checker accept the function, by using structurally smaller list xs' while calling parseDriver' recursively.

parseDriver : String -> Maybe Char
parseDriver s = parseDriver' chars chars where
  chars : List Char
  chars = unpack s

  -- 2nd parameter is a dummy one (to make totality checker happy)
  parseDriver' : List Char -> List Char -> Maybe Char
  parseDriver' _  [] = Nothing
  parseDriver' xs (_::xs') =
    case parse xs of
      Jump j => parseDriver' (drop j xs) xs'
      Return x => Just x
      Error => Nothing

We could've also used some natural parameter n, which we could decrement at each step, making sure we stop at 0. The initial value of n could naturally be the length of the input list.