Currently, the presence of axioms is checked at the end of the Core pipeline when a lot of processing has already been done. When you e.g. forget to remove todos, this can result in cryptic error messages not pointing to actual source positions, like
/core-check:1:1: error:
The function lambda_22@Kudos.MetaMask uses an axiom and thus it cannot be compiled
The presence of axioms should be checked earlier, preferably around type-checking (only when actually compiling). The errors should point to where in the source the axiom is used. This is a bit tricky, because we'd need to filter for reachable definitions at this point (but I recall there is already some infrastructure for it).
Currently, the presence of axioms is checked at the end of the Core pipeline when a lot of processing has already been done. When you e.g. forget to remove
todos, this can result in cryptic error messages not pointing to actual source positions, likeThe presence of axioms should be checked earlier, preferably around type-checking (only when actually compiling). The errors should point to where in the source the axiom is used. This is a bit tricky, because we'd need to filter for reachable definitions at this point (but I recall there is already some infrastructure for it).