Remove indirections to builtins/primitives in `QName`
We currently share the QName between abstract and internal syntax.
However, after scope checking we could resolve all the BUILTINs and primitives to their special identifier, so that I.QName could directly tell us which builtin we deal with (if any).
This would have the advantage that we could work with builtins in pure code, e.g. in smart level constructors.
We would also shave off some cycles by not always having to call getBuiltin.
I expect such refactoring could fix the following issue without performance penalty:
- #8100
Agda dev meeting 2025-10-15: Alternative: have nicifier lift BUILTINs so that we can already in the scope checker resolve builtins. However, we have a problem with BUILTIN NATURAL / MAYBE as the constructors are resolved to the ZERO/SUC etc builtins by type. Suggestion: bring back BUILTIN NATZERO etc.