[ fix ] performance issue in totality checking

[dunhamsteve]

This PR addresses an exponential slowdown issue in totality checking and fixes #3696.

Issue

The following code takes appears to freeze during totality checking of foo:

bar : (a, b, c, d, e : Unit) -> Unit

foo : (n : Nat) -> Unit
foo 100 = id $ bar () () () () () 
foo _ = ()

bar _ _ _ _ _ = foo 0

Root cause

Here the term bar () () () () () appears as an argument on the RHS. Idris tries to determine if it is smaller than an argument on the left. The LHS has a large Nat. Size compare falls through to the case where we check a constructor application in the pattern (t) against the application of bar. This recurses to checking the function application against each of the arguments of that constructor:

Idris2/src/Core/Termination/CallGraph.idr

Lines 218 to 223 in 6a54860

	sizeCompareCon fuel s t
	= let (f, args) = getFnArgs t in
	case f of
	Ref _ (DataCon t a) cn =>
	-- if s is smaller or equal to an arg, then it is smaller than t
	if !(sizeCompareConArgs (minus fuel 1) s args) then pure True

And if sizeCompareCon fails, we hit fallback code that calls sizeCompareApp, which peels off an argument of the function and runs the entire process again, comparing bar () () () () to 100.

Idris2/src/Core/Termination/CallGraph.idr

Lines 241 to 242 in 6a54860

	sizeCompareApp fuel (App _ f _) t = sizeCompare fuel f t
	sizeCompareApp _ _ t = pure Unknown

So we end up running:

• sizeCompare (bar () () () () ()) (S (S (S ...))
  • sizeCompare (bar () () () () ()) (S (S ...)) (peel off an S in sizeCompareCon)
    • sizeCompare (bar () () () () ()) (S (S ...))
      • ...
      • ...
    • sizeCompare (bar () () () ()) (S (S ...))
      • ...
      • ...
  • sizeCompare (bar () () () ()) (S (S (S ...))) (peel off the () in sizeCompareApp)
    • sizeCompare (bar () () () ()) (S (S ...)) (remove S in sizeCompareCon)
      • ...
      • ...
    • sizeCompare (bar () () ()) (S (S (S ...))) (peel off the () in sizeCompareApp)
      • ...
      • ...

Which is exponential and redundant.

Fix

The Foetus paper has a rule like "if y ρ x then (y a) ρ x" (for ρ in <,=). So we do need to check prefixes of the application, but we can do this at the leaves. Instead of rerunning everything in sizeCompareApp, check whether the LHS is equal or a prefix of the RHS as a function application. Deeper recursion is handled by the earlier branch, going under the constructor.

Self-check

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md
• I confirm that this contribution did not involve GenerativeAI nor Large Language Models.