Is this a limitation of the Idris totality checker, or am I missing something?

Question

Idris claims the following code is not total:

data Foo = Bar (Maybe Foo)

foos : Foo -> List Foo
foos (Bar (Just foo)) = foo :: (foos foo)
foos (Bar Nothing) = Nil

Instead I can do

foos t@(Bar (Just foo)) = foo :: foos (assert_smaller t foo)

but this seems unnecessary. Obviously the first Foo I create must be constructed as Bar Nothing, and subsequent constructions can only be constructed in the same way or from existing terms, and so this should always terminate.

Is there some similar case where totality cannot be decided, or is Idris not yet able to handle this type of situation?

Answer 1

You are correct. Idris is not yet able to handle this type of situation.