[ new ] totality checking can look under constructors

[dunhamsteve]

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.

[mjustus]

It is not clear to me whether it is sound to make applied type constructor of the same name size-equal regardless of their arguments. But I did not manage to come up with a counter-example (assuming a putative Idris with universe levels/universe polymorphism).

Do you have an intuition why this is correct?

[dunhamsteve]

I think at the time I was considering them irrelevant. I'm asking for things to be the same or smaller when we go under a constructor, and that was my way of ignoring the implicit type arguments.

I think we would have been ok here for now because we don't look under TyCon to determine something is smaller. So if the type got bigger it could still never cause the function to be counted as total.

I've changed it to check the arguments, expecting everything to be the Same or Smaller. It's still contributing Same at best. So, like the status quo, pulling something out from under a TyCon doesn't count as Smaller.

  sizeCompareTyCon fuel s t =
    let (f, args) = getFnArgs t in
    let (g, args') = getFnArgs s in
    case f of
      Ref _ (TyCon _ _) cn => case g of
        Ref _ (TyCon _ _) cn' => if cn == cn'
            then (Unknown /=) <$> sizeCompareProdConArgs fuel args' args
            else pure False
        _ => pure False
      _ => pure False

[mattpolzin]

This looks good and well analyzed to me; do @mjustus or @gallais want to take a look at this before merging?