[ regression ] Totality checker no longer accepts certain total functions

[stefan-hoeck]

Looks like this is a regression (?) introduced by #2953 . The following proof from idris2-algebra is no longer accepted by the totality checker. Using @-patterns seems not to work here either, and I'm currently uncertain how to proceed with this.

This is the function in question but I'll try to come up with a self-contained example later today. Note that this is currently blocking (amongst some other libraries probably failing for similar reasons) the generation of nightly pack collections.

  -- Adding two sums via `add` preserves the evaluation result.
  export
  0 padd : (x, y : Sum a as) -> esum x + esum y === esum (add x y)
  padd []            xs = r.plus.leftNeutral
  padd (x :: xs)     [] = r.plus.rightNeutral
  padd (T f x :: xs) (T g y :: ys) with (compProd x y) proof eq
    _ | LT = Calc $
      |~ (f * epr x + esum xs) + (g * epr y + esum ys)
      ~~ (f * epr x) + (esum xs + (g * epr y + esum ys))
        ..< r.plus.associative
      ~~ f * epr x + esum (add xs (T g y :: ys))
        ... cong (f * epr x +) (padd xs (T g y :: ys))
    _ | GT = Calc $
      |~ (f * epr x + esum xs) + (g * epr y + esum ys)
      ~~ g * epr y + ((f * epr x + esum xs) + esum ys)
         ..< lemma213 r.plus.csgrp
      ~~ g * epr y + esum (add (T f x :: xs) ys)
         ... cong (g * epr y  +) (padd (T f x :: xs) ys)
    _ | EQ = case pcompProd x y eq of
         Refl => Calc $
           |~ (f * epr x + esum xs) + (g * epr x + esum ys)
           ~~ (f * epr x + g * epr x) + (esum xs + esum ys)
             ... lemma1324 r.plus.csgrp
           ~~ (f + g) * epr x + (esum xs + esum ys)
             ..< cong ( + (esum xs + esum ys)) r.rightDistributive
           ~~ (f + g) * epr x + esum (add xs ys)
             ... cong ((f + g) * epr x +) (padd xs ys)

[mjustus]

I am fairly certain this is due to #2954. Prior to PR #2953, the termination checker was accepting some functions for the wrong reason, masking issue #2954.

I am currently preparing a refinement to the termination checker that represents size-graphs as matrices. It's still work-in-progress but idris2-algebra does seem to build. I'd be curious which other libraries no longer pass the termination checker.

[stefan-hoeck]

I am fairly certain this is due to #2954. Prior to PR #2953, the termination checker was accepting some functions for the wrong reason, masking issue #2954.

I am currently preparing a refinement to the termination checker that represents size-graphs as matrices. It's still work-in-progress but idris2-algebra does seem to build. I'd be curious which other libraries no longer pass the termination checker.

Thanks for working on this. In that case I think I'll temporarily use assert_smaller in idris-algebra until your fix lands. I'll see what else in the pack collection fails. I'll report back here if anything interesting shows up.

[mjustus]

I have now merged my changes to the termination checker. Unfortunately, they do not address this particular termination issue. The problem here is caused by the with-abstraction, see #403.

The program first deconstructs the Sum (T f x :: xs), for example, and then reconstructs it in the recursive call padd (T f x :: xs) ys. The recursive call appears under a with-abstraction so gets lifted to an auxiliary top-level function, which gets passed only the constituent parts of the Sum. As far as the termination checker is concerned, this generated function therefore increases the sizes of arguments f, x, xs by calling padd on (T f x :: xs).

There are two potential solutions to this: either we inline with-abstractions during size-graph generation, which is already done for lifted case-functions

https://github.com/idris-lang/Idris2/blob/a26766e57ac5466947903a626082e950ae84192e/src/Core/Termination/CallGraph.idr#L316-L321

or we start counting the number of constructors we strip off/add as part of the size graph. The latter is what Agda does according to @gallais but I suspect this approach will still struggle with deep pattern matches like the one above.

In the meantime, you could write the with-abstraction by hand but pass around the "full" Sum, not just its parts.