[ new ] totality checking can look under constructors

This is another attempt at PR #3328, which addresses #3317. PR #3328 was merged but later reverted because of a performance regression in some cases (#3354 - the compiler hangs). The approach here is the same as #3328 with fuel added.

The change allows Idris totality checker to recognize when data underneath a constructor becomes smaller:

Just xs is smaller than Just (x :: xs)
x :: zs is smaller than x :: y :: zs
(b :: c :: es) is smaller than (a :: b :: c :: d :: es)

The value is considered smaller when constructors match and all of the corresponding arguments are at least Smaller or Same, and at least one argument is Smaller. We can't allow Unknown for any argument for the reason shown in the last test case in Totality.idr (two mutual functions that make different arguments smaller/bigger). This rule is a fallback backtracking behavior after the existing rule fails (which goes under the constructor on the LHS and looks for anything Same or Smaller than the RHS, ignoring Unknown).

Unfortunately this backtracking was exponential in the size of the LHS and structures like the number 64 are big enough to make that very expensive. I do not know of a way to make this not exponential, so I've adopted @buzden's suggestion of using fuel. The fuel controls how deep we can go under constructors before we stop applying the new rule. The existing rule continues to any depth. For most use-cases we do not need to apply the new rule very deeply, so it is still useful. The first two cases above work with a limit of 1, and the last one needs a limit of 3 so we can go under the (::) c _ on both sides.

I've tentatively set the limit to 5 as a tradeoff between performance and utility, but we can pick a different number. The slowdown for this only occurs in cases like #3354. I did not observe slowdown while compiling Idris with #3328, which had unlimited backtracking.

I've added the pragma %totality_depth to allow the user to control the search depth. There is a test demonstrating the use of the pragma and a test for #3354. If there is a better name for the pragma, let me know. The documentation has been updated to include it.

To gauge the performance impact when we hit cases like #3354, I made a file with 100 copies of the following code from #3354 and timed it with thetime utility.

total
g' : Fin 64 -> Unit
g' FZ        = ()
g' i@(FS i') = g' $ assert_smaller i $ weaken i'

The results are in the table below, the first line is how Idris performs without this change, the third column provides an example of what is enabled at each level of fuel for the first few values:

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 for max depth of 5, it takes about 18% longer in situations like #3354, if we decide on a default max depth of 3, then it's about 6% longer when we hit these cases. With #3328 the compile would not terminate when hitting a case like #3354, and this did not happen when building Idris and running the tests.

idris-lang / Idris2

[ new ] totality checking can look under constructors #3362