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.