[ re #5264 ] Make more flags infective

Specifically: `--type-in-type`, `--omega-in-omega`, `--injective-type-constructors`, `--experimental-irrelevance`, `--cumulativity`, and `--allow-exec`

CHANGELOG.md

@@ -44,6 +44,13 @@ Changes to type checker and other components defining the Agda language.
   As in a `with`, multiple bindings can be separated by a `|`, and variables to
   the left are in scope in bindings to the right.
 
+* The following options are now considered infective:
+  `--rewriting`, `--type-in-type`, `--omega-in-omega`,
+  `--injective-type-constructors`, `--experimental-irrelevance`,
+  `--cumulativity`, and `--allow-exec`. This means that if a module
+  has one of these flags enabled, then all modules importing it must
+  also have that flag enabled.
+
 Reflection
 ----------
 

src/full/Agda/Interaction/Options/Base.hs

@@ -1188,6 +1188,12 @@ infectiveCoinfectiveOptions =
   , infectiveOption optCohesion               "--cohesion"
   , infectiveOption optErasure                "--erasure"
   , infectiveOption optErasedMatches          "--erased-matches"
+  , infectiveOption (not . optUniverseCheck)  "--type-in-type"
+  , infectiveOption optOmegaInOmega           "--omega-in-omega"
+  , infectiveOption optInjectiveTypeConstructors "--injective-type-constructors"
+  , infectiveOption optExperimentalIrrelevance "--experimental-irrelevance"
+  , infectiveOption optCumulativity           "--cumulativity"
+  , infectiveOption optAllowExec              "--allow-exec"
   ]
   where
   cubicalCompatible =

test/interaction/Debug.out

@@ -7,8 +7,8 @@
 (agda2-verbose "Wrote interface file. ")
 (agda2-verbose "Accumulated statistics. ")
 (agda2-verbose "Finished Debug. ")
-(agda2-verbose " current options = [--safe: False, --without-K: False, --cubical-compatible: False, --no-universe-polymorphism: False, --no-cumulativity: True, --level-universe: False, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False, --flat-split: False, --cohesion: False, --erasure: False, --erased-matches: False] ")
-(agda2-verbose " imported options = [--safe: False, --without-K: False, --cubical-compatible: False, --no-universe-polymorphism: False, --no-cumulativity: True, --level-universe: False, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False, --flat-split: False, --cohesion: False, --erasure: False, --erased-matches: False] ")
+(agda2-verbose " current options = [--safe: False, --without-K: False, --cubical-compatible: False, --no-universe-polymorphism: False, --no-cumulativity: True, --level-universe: False, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False, --flat-split: False, --cohesion: False, --erasure: False, --erased-matches: False, --type-in-type: False, --omega-in-omega: False, --injective-type-constructors: False, --experimental-irrelevance: False, --cumulativity: False, --allow-exec: False] ")
+(agda2-verbose " imported options = [--safe: False, --without-K: False, --cubical-compatible: False, --no-universe-polymorphism: False, --no-cumulativity: True, --level-universe: False, --cubical/--erased-cubical: False, --guarded: False, --prop: False, --two-level: False, --rewriting: False, --sized-types: False, --guardedness: False, --flat-split: False, --cohesion: False, --erasure: False, --erased-matches: False, --type-in-type: False, --omega-in-omega: False, --injective-type-constructors: False, --experimental-irrelevance: False, --cumulativity: False, --allow-exec: False] ")
 (agda2-verbose " Now we've looked at Debug ")
 (agda2-status-action "Checked")
 (agda2-info-action "*All Done*" "" nil)