const-computations, comptime

Some parts of modules are executed:

• at parse time: e.g. notations? Expanded before getting a HOAS tree.
• at expand time: macros get expanded after having a HOAS tree, before starting compilation
• at compile time: source code undergoes typechecking; the universe of types is expanded by definitions.
• at runtime: it computes.

Macros and notations should not be reprogrammable on the fly; ideally, they should be fixed for a package and known beforehand when depending on it. No conditional notations (and macros?).

Q: should packages have a clearly separate section for parse/expand-time things? Q: how to delineate compile/run time contexts in the code?
Q: Should comptime operations be a subset of runtime operations? Can all types be projected into runtime? If so, how?