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?
[x] 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).
Description
The PR enhances totality checking to see size changes underneath matching constructors, addressing issue #3317. With this change Idris recognizes:
Just xsis smaller thanJust (x :: xs)x :: zsis smaller thanx :: y :: zsand 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
SameorSmaller(notUnknown), and at least one argument isSmaller. This is applied recursively, soa :: c :: esis smaller thana :: 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
pfoomfunction in two of the existing tests are now accepted as total. I believe this is correct, sinceC0 xis smaller thanC0 (C1 x).Further Details
Additionally, we have to traverse meta solutions. In the case of
Just xsis smaller thanJust (x :: xs)atMaybe (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 getUnknownwhen comparing the implicit in the pattern against the meta on the RHS. Changing the normalization to addholesOnlycauses the testperf003to 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
sizeComparewhen 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 withsizeEq(which checks that they're the same meta with equal arguments). I did not push this down intosizeEqbecause traversing the meta requires returningCoreandsizeEqis passed toeqBinderBy.If we have application of the same type constructor on both sides,
sizeCompareis calling them theSamesize without recursing into the arguments. In the example, this handles the implicit argument ofJust(which isList 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 theperf003test, so I don't think this is affecting performance.Should this change go in the CHANGELOG?
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).