[ refactor ] Port Yaffle's Value

[GulinSS]

This PR tracks the ongoing effort to port Yaffle into the Idris2 codebase.

Work in progress — This PR is primarily for tracking progress. The current state is outdated and incomplete.

This PR requires the following to be merged first: #3513

PR commits will be squashed into a series of less number of commits to improve maintainability during rebases and ease review.

---

Squashed, origin: https://github.com/GulinSS/Idris2/tree/core-evaluate-value/all-no-compact

[GulinSS]

Well, it was hard to rebase but still need some care to clean up comments, logs and so on. It was hard... no much to say for now. 😅

[haskiindahouse]

We've been building on a minimal slice of this PR (lineage around ca73c33) and stress-testing the new-core totality checker against deptycheck-style code: deeply indexed types, large derived generators, heavy erased proof arguments. Three findings that may be useful for the port, all with small repros; fix branches are public on our fork (haskiindahouse/Idris2).

1. False "possibly not terminating" from erased (Rig0) proof arguments.
findSC descends into erased argument expressions at call sites. In deptycheck's Test.DepTyCheck.Gen SCC this yields 29 false not-total verdicts (map, <**>, >>==, Monad Gen, …) for code the current master checker accepts. The mechanism we observed: evaluated erased proof args (e.g. (0 _ : IsNonEmpty (g >>== f))) produce disconnected skolems → all-Unknown rows in the size-change matrices → SCT failure. scEqSpine already ignores erased spine entries, but findSC's descent does not — the inconsistency is the bug. Fix branch: opus/eskcall.

2. …but skipping erased args naively is unsound.
A blanket "skip erased args in findSC" accepts this:

data Empty : Type where

step2 : (0 contra : Empty) -> Empty
step2 _ impossible

total
falseEmpty : Empty
falseEmpty = step2 falseEmpty   -- accepted total with a naive skip; rejected by master

After testing both extremes (a blanket skip is unsound; keeping all self-edges from erased args reintroduces the 29 false positives), the rule we landed on: inside an erased argument, descend only when the argument is headed by a direct application of the function under size-change check, and keep only those self-edges (branch opus/soundfix). That keeps the false-positive fix and rejects the repro above. Separately: the unpatched PR head already accepts total006's badCount as total — a pre-existing draft issue worth tracking.

3. Deep-pattern performance cliff in getSC.
Large literal/constructor patterns alone trigger ~n^4.5 behavior, no RHS applications needed: foo 1000 = () checks in ~0.9s on master but effectively hangs on the new core (n=200/300/400 → 4.8/28/108s). We localized it to per-pattern-level argument-list growth/rescans around findSCscope/replaceInArgs/canonicalise; a fix attempt is in progress on the fork. Notably, the old core's exponential from #3696 is absent here — the new pre-collected-spine sizeCompareApp already has the fixed shape (the #3696 repro checks ~80× faster on this port than on master).

Happy to upstream any of this as patches once the port stabilizes; repros and branches are on the fork.

[GulinSS]

@haskiindahouse please attach a link with a suggested fix to each issue from the list of your comment.

As for now I was able to determine only a fix for issue 1 and a fix for issue 2.

Is it correct?

[haskiindahouse]

@GulinSS yep, correct

but special for you: I've cleaned these up into two self-contained branches off ca73, so each fix is a single commit touching only the totality checker, with the unrelated perf/memoise work stripped out.
Per-issue mapping:
Issues 1 and 2 — one combined fix:

totality/erased-arg-soundness(https://github.com/haskiindahouse/Idris2/tree/totality/erased-arg-soundness) (173bd02)
findSC was descending into erased (Rig0) argument expressions even though scEqSpine already ignores erased spine entries — that's what produced the false "possibly not terminating" verdicts. A blanket skip would be unsound (it accepts total falseEmpty : Empty via erased recursion), so the rule is: inside an erased argument, descend only when it's headed by a direct application of the function under size-change check, keeping only those self-edges. So your "fix for 1" and "fix for 2" are really this one commit — the naive skip and the soundness refinement folded together. It removes the false positives and still rejects the falseEmpty / erased-IH cases (and keeps the non-erased Control baseline rejected).

Issue 3 — the part that was out of date: totality/getsc-cliff (https://github.com/haskiindahouse/Idris2/tree/totality/getsc-cliff) (9726ce8)

When I first commented there was no branch ("fix attempt in progress"); there is one now. A deep literal/constructor pattern alone (e.g. foo 1000 = ()) drove getSC into ~n^4.5; this records case splits as forced equations with entry copies bounded by re-match events rather than pattern depth, bringing it back to ~n². It's CallGraph.idr-only and independent of the soundness change — it cherry-picks cleanly onto ca73 on its own.

Caveats, so nothing's oversold:

• The soundness fix narrows but doesn't fully close things: a self-call nested strictly under a foreign head inside an erased argument, and mutual recursion routed exclusively through erased arguments, still slip through — probably worth a separate issue.
• Unrelated to these: the unpatched PR head already accepts total006's badCount as total, a pre-existing item.
• The cliff timings are from my own benchmarking. I can also add the repros (the erased-IH / falseEmpty cases and a deep-pattern test) as in-tree tests if you'd like them reproducible from the branch.