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.

[mjustus]

The termination checker only looks for structurally smaller arguments. Working up to "matching constructors with structurally smaller arguments" would actually be a very simple change: sizeCompareCon needs to recurse on arguments when s and t start with the same constructor.

[hyphenrf]

Should I attempt this addition then? I'll happily prepare a PR

[buzden]

Should I attempt this addition then? I'll happily prepare a PR

You definitely should!

[dunhamsteve]

I had looked into this over the last two days and the logic is working, but I ran into a snag (you have to apply the change below for the test to pass, but then perf003 fails):

https://github.com/idris-lang/Idris2/compare/main...dunhamsteve:Idris2:total2?expand=1

The rule I'm using is:

Constructor matches, all arguments are either equal or smaller, and at least one is smaller. So no Unknown allowed. I believe you can sneak in bigger values if you allow Unknown arguments to the constructor.

The issue I hit is that there are some metas in a case like Just (xs) < Just (x :: xs) (At Maybe (List a)) The meta is solved but the normalization isn't substituting the result in. (So it is Unknown when comparing against the one in the pattern.) If I change the tcOnly normalization from withArgHoles to withHoles in Value.idr it all works great:

 tcOnly : EvalOpts
-tcOnly = { tcInline := True } withArgHoles
+tcOnly = { tcInline := True } withHoles

But the perf003 test never finishes. So I've got a performance regression.

The only difference between argHolesOnly and holesOnly that I can find is in Eval.idr around line 500, and it looks like it's exactly the case of an erased argument that argHolesOnly suppresses.

[buzden]

@dunhamsteve, just a guess: maybe you should try what you are doing upon #3272

[dunhamsteve]

It looks like the issue is in the normalization itself. I took out all of my changes and added one very targeted change:

findCalls defs (_ ** (env, lhs, rhs_in))
    = do let pargs = getArgs (delazy defs lhs)
-        rhs <- normaliseOpts tcOnly defs env rhs_in
+        rhs <- logTime 1 "tcOnly" $ normaliseOpts ({ holesOnly := True} tcOnly) defs env rhs_in
         findSC defs env Toplevel pargs (delazy defs rhs)

The test looks like:

0 IdType : Type
IdType = {0 a : Type} -> a -> a

id : IdType
id = \ x : _ => x

idid : {0 a : Type} -> a -> a
idid = id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id
       id id id id id id id id id id

It's exponential in the number of id, each additional id doubles the time logged:

ids	ms
20	1101
21	2198	1.996
22	4371	1.988
23	8733	1.998
24	17574	2.012
25	35374	2.013
26	72390	2.046

Aside from the test though, the totality checking works well. :)

(And building idris2api.ipkg does not slow down with that change.)

[mjustus]

The length of the largest implicit argument a doubles with each additional id so once you start inlining the corresponding meta-variable(s) the size of the overall term blows up exponentially.

There are some real code bases where this behaviour occurs naturally so inlining all solved meta-variables for termination checking is unlikely to be feasible.

Before #2977 was merged, I was traversing meta-variable solutions during termination checking and that seemed to be fast enough. Sadly, I can't find that code right now but it would be easy enough to reproduce.

[dunhamsteve]

I think I've got the meta traversal working right and updated the branch.

It's passing my tests and perf003. I had to wire defs and the Core monad into some of the code. I kept it out of sizeEq because it was passed to a HOF, and did the expansion in compareSize instead. I'm only expanding metas on the RHS and letting sizeEq handle Meta/Meta comparison. (Do metas show up in patterns? Maybe inside dotted expressions?)

The time for a full idris2api compilation doesn't seem affected by this change, and the perf003 test time seems the same too.

One thing I did do for expediency is consider type constructor applications to be the Same quantity without digging into arguments. I could run them through the same process as data constructors if this is an issue.