Check on presence of --erasure in --erase-record-parameters comes too early #6573
Description
The test for presence of --erasure in the activation code for --erasure-record-parameters
agda/src/full/Agda/Interaction/Options/Base.hs
Lines 1036 to 1039 in e4b6c53
isn't lazy enough:
$ agda --erase-record-parameters
Error: The option --erase-record-parameters requires the use of --erasure
...
$ agda --erase-record-parameters --erasure
Error: The option --erase-record-parameters requires the use of --erasure
@nad, you introduced this check in 1e5dd29. Before this commit, --erasure-record-parameters would imply --erasure. You didn't give a reason for this change in the option logic in this commit. However, I found some discussion in #6350 (comment).
There you complain (rightfully) that if X implies Y, then X followed by no-X will turn on Y without X being on in the end.
This problem exists still for --flat-split implying --cohesion, so maybe we need a systematic solution and a uniform strategy.
An improvement would be to only check for option consistency after we parsed all command line options.
However, maybe implication should in general be resolved at use site only, so, much more lazily and declaratively. E.g. whenever we query whether we have --cohesion, we check whether we have either --cohesion or --flat-split.
Note: I am currently working on a refactoring of the options, this is where I came across this issue.