Overhaul dead code elimination, make --save-metas the default

[AndrasKovacs]

• Fix #7058 by rewriting most of dead code elimination.
• Make --save-metas the default.

Dead code elimination now does the following:

• eliminateDeadCode computes and returns collections of reachable definitions and metas. It does not instantiate anything and has no side effect. The roots for reachability are the following:
  • Public definitions and pattern synonyms
  • Definitions with COMPILE pragma
  • Primitive definitions
  • Parameter sections of public modules
  • Local builtins
  • All rewrite rules
• In buildInterface, we instantiateFull the output interface if we have --no-save-metas.

Moreover, --save-metas is now made default. Reasons for doing so:

• Future optimizations of meta instantiations critically depend on --save-metas, and --no-save-metas should eventually become deprecated in favor of finer control over meta inlining.
• Hence, --save-metas should be the config that's being continuously tested. While making this branch, I discovered that make test actually failed with --save-metas because of an unrelated bug in NamesIn (which is fixed here).
• Benchmarks on my machine (AMD 7700X, DDR5 6000):
  • std-lib: checking time 5.4% shorter (204.27 -> 192.8 s), interface size +1.83% (168.9M -> 172M).
  • cubical lib checking time 0.7% longer (622.600 -> 627.2 s), interface size +4.6% (153M -> 160M).

In short there's a significant performance win in std-lib and an insignificant loss in cubical. I'd consider the interface size diffs to be also insignificant.

Right now, part of the small impact of --save-metas is that all definition bodies are instantiateFull-ed by elaboration in Agda.TypeChecking.Rules.Def. So far, I think that the following metas can survive elaboration: those in function clause LHS-es, rewrite rules, display forms, module parameter sections, and some metas in definitions bodies, those that become solved later by elaborating other things in a mutual group.

[AndrasKovacs]

@plt-amy I'd like to benchmark this on 1lab, what's the best way? I asked this from you before but I don't find where I did.

[plt-amy]

You can do env AGDA=/what/ever AGDAFLAGS='whatever' bash support/check.sh

[AndrasKovacs]

More or less as expected, we OOM on 1lab.HIT.Truncation as described in #7231.

[plt-amy]

To summarize the discussion there/our findings from the AIM, the issue is essentially that keeping around the telescopes for solved (primarily instance) metas in macros leads to quadratic duplication of intermediate results:

foo : {{ _ : Class }} → TC ⊤

test : TC ⊤
test = do
  x ← something -- imagine it produces a very big result
  foo {{ ?inst ... x }}

After evaluating something and bindTC, we're looking at foo {{ ?inst ... [very big result ] }}, and this result is further duplicated in every bind that happens after something. I think this doesn't usually matter, but if something has to traverse the term (like addContext, for the escape check), it's explosive.

[AndrasKovacs]

@plt-amy

• In #7231 there's a link for instantiated and non-instantiated terms here; neither term looks like it should cause OOM or hanging. Do we know that the issue is just non-instantiated term size there, or some actual freeIn bug?
• Is it true that TC-produced terms are generally not instantiated, unlike ordinary definitions?

[plt-amy]

AIUI the problem isn't in the generated terms, but rather in the macros themselves — the duplicated intermediate results are present in meta telescopes in suspended computations (after using e.g. blockTC), and the results of TC computations. As for the actual root cause, I can't say: the uninstantiated term is ~5× bigger (printed) than the instantiated term, but we didn't perform any investigation other than "instantiateFull fixes it" (and looking for ⦃ ... ⦄ and going "huh, that shouldn't be there").

(Of course, #7231 should be updated to normalise the intermediate result, since otherwise you get false positives for local variables that would evaluate away; this is unrelated, but also fixes the OOM).