Reconstructing a (structurally smaller) aggregate from pattern-matched components trips up the totality checker

[hyphenrf]

Steps to Reproduce

I was trying this with a simple list and a NonEmpty predicate, but here's a minimal example without it:

total
f : (a, List a) -> ()
f (_, []) = ()
f (x, _::xs) = f (x, xs)

It's possible to prove this terminates with Control.WellFounded, however, add some complexity going back to my original attempt:

import Data.List
import Control.WellFounded

total
f :  Eq a => (xs : List a) -> { auto p : NonEmpty xs } -> Nat
f (x::xs) with (sizeAccessible xs)
  f [_] | _ = 1
  f (x::y::zs) | Access r =
    if x /= y
       then f (x::zs) | r _ reflexive
       else S (f (x::zs)) | r _ reflexive

and it fails with a couple of strange error messages which I highlight below.

Expected Behavior

Idris can see that xs is in fact smaller than _::xs, without much intervention from my side. Also whatever caused the strange error messages in wellfounded approach be addressed.

Observed Behavior

First (simple) attempt:

Error: f is not total, possibly not terminating due to recursive path Main.f

A sprinkle of WellFounded makes Idris happy again.

Second (more complex) attempt:

• if you leave the else branch S (...), it fails highlighting x::xs and complaining: Error: With clause does not match parent
• however, change it to S $ ... or 1 + ... and a better(?) error message emerges, about both branches missing holes that need to be filled, I abbreviated the error messages, taking note to keep only the ^^^-highlighted section of the code:

  Error: Unsolved holes:
  Main.{_:1988} introduced at: f (x::zs) | r _ reflexive
  Main.{_:2018} introduced at: S $ f (x::zs) | r _ reflexive
  

  ... I feel like that should be a bug report on its own?

Circumvention:

f : Eq a => (xs : List a) -> { auto p : NonEmpty xs } -> Nat
f (x::xs) = go x xs
  where go : a -> List a -> Nat
        go _ [] = 1
        go x (y::zs) = if x /= y then go x zs else S (go x zs)

Extra Notes:

I asked this question on an Idris community channel before filing the bug report. Initial reactions were confused. There were suggestions that the totality checker simply makes no attempt to follow function/constructor applications. That made sense to me for functions but not for constructors (in my mind there's nothing preventing that, they're trivially reducible, and the compiler should at least easily know about List, in fact it has a Sized instance for it by default). However, more interestingly:

total
ok : (l : List a) -> {auto _ : NonEmpty l} -> ()
ok [_] = ()
ok (_::x::xs) = ok (x::xs)

partial
no : (l : List a) -> {auto _ : NonEmpty l} -> ()
no [_] = ()
no (x::_::xs) = no (x::xs)

in both cases we have a constructor, but in one case it's "shared" structure, while in the other it's "new". Comparing list lengths should remove that distinction... and I'm not sure if this is the core issue here or just another observed behavior.

Moreover, the fact that NonEmpty is an auto-implicit changes nothing about the above, at least as far as I can tell. I tried different variants of the declaration.