agda
Should more flags be infective (or have coinfective negations)?
While pondering about my proposed fix for #4908, I stumbled upon the following question. Currently, there is a bunch of flags that are disabled by --safe, but are themselves not infective. So currently the only way to disable one of these flags in a file and in all its dependencies is by using --safe, but this is not granular. Specifically, I'm talking about the following flags that are forbidden by --safe but are currently not infective:
-
--allow-unsolved-metas -
--allow-incomplete-matches -
--no-positivity-check -
--no-termination-check -
--type-in-type -
--omega-in-omega -
--injective-type-constructors -
--experimental-irrelevance -
--cumulativity -
--allow-exec
For my fix of #4908, I need to have a way to disable each of these flags selectively in a way that is also respected in all dependencies of the current file. I see two options to achieve this goal:
- One option that I think makes sense would be to make all of these flags infective (or equivalently, make their negations coinfective), so that it becomes possible to disable them for the whole dependency tree. However, this would cause a problem for backwards compatibility.
- An alternative proposal would be to introduce new flags that act like the negations of these flags but are also coinfective. Perhaps these coinfective variants could be prefixed with
--safe, e.g.--safe-positivity-check,--safe-no-type-in-type,--safe-no-cumulativity, etc.
Before I continue with the implementation, I'd like to know what other people think about this. How worried should I be about breaking backwards compatibility in this way? Am I overengineering things by introducing ten new flags that are just coinfective variants of (mostly) already existing flags?
I don't know, I am switching to AI and have not worked on bioinformatics for many months.