[ new ] totality checking can look under constructors

[dunhamsteve]

Description

The PR enhances totality checking to see size changes underneath matching constructors, addressing issue #3317. With this change Idris recognizes:

• Just xs is smaller than Just (x :: xs)
• x :: zs is smaller than x :: y :: zs

and similar changes. The new additional rule is that an argument is smaller than a parameter if the data constructors match on both sides, each of the corresponding arguments of the constructor are either Same or Smaller (not Unknown), and at least one argument is Smaller. This is applied recursively, so a :: c :: es is smaller than a :: b :: c :: d :: es.

We can't allow Unknown, because that could be used to introduce a structurally larger child that could later be used in recursion.

That change is in sizeCompareCon.

The pfoom function in two of the existing tests are now accepted as total. I believe this is correct, since C0 x is smaller than C0 (C1 x).

pfoom : Bin -> Nat
pfoom EPS = Z
pfoom (C0 EPS) = Z
pfoom (C0 (C1 x)) = S (pfoom (C0 x))
pfoom (C0 (C0 x)) = pfoom (C0 x)
pfoom (C1 x) = S (foom x)

Further Details

Additionally, we have to traverse meta solutions. In the case of Just xs is smaller than Just (x :: xs) at Maybe (List a), some of the implicit arguments on the right side are metas. The normalisation for totality checking does not substitute erased metas, so with that change alone, we get Unknown when comparing the implicit in the pattern against the meta on the RHS. Changing the normalization to add holesOnly causes the test perf003 to timeout, because a term in the test grows exponentially. So I'm traversing the metas as needed, as suggested by @mjustus.

I'm doing that in sizeCompare when I see a meta on the right hand side and no meta in the pattern. For the case with metas on both sides, I left the current behavior of checking with sizeEq (which checks that they're the same meta with equal arguments). I did not push this down into sizeEq because traversing the meta requires returning Core and sizeEq is passed to eqBinderBy.

If we have application of the same type constructor on both sides, sizeCompare is calling them the Same size without recursing into the arguments. In the example, this handles the implicit argument of Just (which is List a). Let me know if I need to check those arguments for equal or smaller.

Someone needs to double check what I'm doing here, when they find time. Possibly @mjustus, who has worked on the totality checker recently.

Performance impact: I don't see a change in the full compilation time for idris2api.ipkg (measured by /usr/bin/time) nor for the time reported by the perf003 test, so I don't think this is affecting performance.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[gallais]

This is the scary part IMO: if the first check fails, we run some further checks that
are at least as big. In the unhappy path we potentially go from linear to exponential.

[dunhamsteve]

I saw this might be exponential in the size of the thing on the left side, but didn't see any slowdown when building Idris itself. (I considered cutting quicker on line 212 - which could still be exponential, but didn't see a slowdown.) I believe things are getting structurally smaller there. (Assuming getFnArgs is returning parts of the whole.)

But the part about @buzden's test case that confuses me is the expression on the left side is small. It doesn't look like any expression is big in the example, it must be looping somewhere. (Edit: I'd just woken up and glossed over the 64 bit.)

Sorry about that, I'll take a look tonight and this weekend, but fixes are welcome.

[dunhamsteve]

But I'm inlining meta solutions in sizeCompare. I suspect that's going to be involved.

[dunhamsteve]

I don't see a way to avoid the exponential bit. We're comparing different things on either side of the if so there isn't information / computation to be shared. (We're going inside one constructor in the first case and both in the second case.)

So I'm thinking @buzden's suggestion of adding fuel is the way to go. The fuel would decrement when going under a constructor on the LHS, but we would continue with current behavior when out of fuel.

I timed this by putting 100 copies of @buzden's problem in a file and got:

fuel	seconds	accepts
0	1.10	status quo: xs < x :: xs
1	1.10	Just xs < Just (x :: xs)
2	1.12	(a :: b :: es) < (a :: b :: c :: es)
3	1.17	(a :: c :: es) < (a :: b :: c :: d :: es)
4	1.21
5	1.30
6	1.50
7	1.89
8	2.64
9	4.10
10	6.94
10	12.30
12	22.68

So a fuel of one could go under a single Just and larger fuel can look deeper under matching data structures. I don't know that we need to go much deeper than 3 or 4. I think I've seen cases in the ncurses code where the decreasing value is 2-3 deep, and my deepest test case requires a fuel of 3. I put a pragma in my proof of concept to allow the user configure the max depth. I've tentatively named the pragma%totality_depth and set the default to 5.