Cleanups in real numbers

[lowasser]

I started out wanting to make some parameters implicit, now that with opaque definitions they can reliably be inferred from the context.

Then things snowballed from there to include a bunch of #1545, use of abstract opaque, and elimination of redundant imports.

[fredrik-bakke]

Have you made any measurements wrt. the performance impact of these changes? One thing that worries me is that, even though Agda may be able to infer certain arguments, doing so may take nontrivial amounts of typechecking time and memory. This for instance led to the recent memory issue #1577. Though, in that case nothing was marked abstract or opaque, so your changes might work well with Agda.

[fredrik-bakke]

Conditional approval, depending on that the performance is not drastically worse than before.

[lowasser]

Have you made any measurements wrt. the performance impact of these changes? One thing that worries me is that, even though Agda may be able to infer certain arguments, doing so may take nontrivial amounts of typechecking time and memory. This for instance led to the recent memory issue #1577. Though, in that case nothing was marked abstract or opaque, so your changes might work well with Agda.

I have not measured it, but the overwhelming majority of users of these functions were already passing _ and allowing Agda to infer the values, so I'm disinclined to sweat it.

[lowasser]

A clean build on my machine took 30 seconds less after this PR for some unclear reason, so I'm pretty confident this doesn't do anything disastrous.

[fredrik-bakke]

FYI we have the scripts/remove_unused_imports.py script to automate the import optimization. I went ahead and ran it on the files you touched.

[fredrik-bakke]

A clean build on my machine took 30 seconds less after this PR for some unclear reason, so I'm pretty confident this doesn't do anything disastrous.

That's amazing, great work!