Save-metas causes OOM during macro execution

[plt-amy]

As discussed in the Agda meeting today, checking the 1Lab with --save-metas runs out of memory (even on my desktop with 128 GiB!). Using --trace-imports, I narrowed this down to 1Lab/HIT/Truncation, and running with a few verbosity flags, I'm pretty sure it starts looping when running ∥-∥³-elim-set — it might eventually get past this, but I killed the save-metas run when memory usage went past 8GiB. Here is the trace; cc @AndrasKovacs.

Sorry for the awful reproducer, but also as discussed, I'm not really in a position to narrow it down any further this week (though cc @ncfavier, who wrote the explosive macro, and might have an idea). If anyone will work on this, keep in mind that the 1Lab only works with master (more specifically, it now needs the instance overlap pragmas).

[plt-amy]

To be clear I killed the save-metas run in this file because checking it successfully has max residency a bit over 1GiB:

  78,604,576,424 bytes allocated in the heap
   9,346,647,992 bytes copied during GC
   1,047,939,672 bytes maximum residency (57 sample(s))
       2,221,480 bytes maximum slop
            2223 MiB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     18826 colls,     0 par    4.783s   4.790s     0.0003s    0.0018s
  Gen  1        57 colls,     0 par    4.125s   4.126s     0.0724s    1.1531s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time   22.201s  ( 22.178s elapsed)
  GC      time    8.909s  (  8.916s elapsed)
  EXIT    time    0.000s  (  0.006s elapsed)
  Total   time   31.110s  ( 31.100s elapsed)

  Alloc rate    3,540,642,516 bytes per MUT second

  Productivity  71.4% of total user, 71.3% of total elapsed

[ncfavier]

https://github.com/agda/agda/pull/7231