title: Is this a limitation of the Idris totality checker, or am I missing something?
body: <p>Idris claims the following code is not total:</p>
  
  <pre><code>data Foo = Bar (Maybe Foo)
  
  foos : Foo -&gt; List Foo
  foos (Bar (Just foo)) = foo :: (foos foo)
  foos (Bar Nothing) = Nil
  </code></pre>
  
  <p>Instead I can do</p>
  
  <pre><code>foos t@(Bar (Just foo)) = foo :: foos (assert_smaller t foo)
  </code></pre>
  
  <p>but this seems unnecessary.  Obviously the first <code>Foo</code> I create must be constructed as <code>Bar Nothing</code>, and subsequent constructions can only be constructed in the same way or from existing terms, and so this should always terminate.</p>
  
  <p>Is there some similar case where totality cannot be decided, or is Idris not yet able to handle this type of situation?</p>