Options used for different modules must be consistent with each other, and options used when loading an interface must be consistent with those used when the interface was created

[identicalsnowflake]

Currently, even in a module marked {-# OPTIONS --safe #-}, you may still import (and use!) primTrustMe and postulates from other modules.

It wouldn't bother me if you could import modules not marked as --safe provided they still follow the safe rules, but it seems currently imported modules are totally exempt from these rules.

[gallais]

I guess it's due to the fact it's the options in the persistent state that get used to typecheck submodules. I don't think we want to modify the persistent state but we could grab the status of the --safe flag right before the call to bracket_ and push it back in after the reset.

Doesn't seem to work.

[gallais]

Minimal test case:

{-# OPTIONS --safe #-}
module Issue2487 where
open import Issue2487-2

module Issue2487-2 where
postulate A : Set

[nad]

This is an instance of a more general problem: Agda does not check that options for different modules in the same project are consistent with each other. For instance, one can use --without-K in one module, and --with-K in another. I suggest that interfaces should contain information about "important" features (various options, use of unsafe features like postulates, and possibly more; perhaps we could even check whether the K rule is used, even when --without-K is not active). When modules are imported one can then check that the imported modules and the importing module use these features in a consistent way:

• Modules using --safe may only import safe modules.
• Modules using --without-K may only import modules that do not use the K rule.
• Other features should also be considered: --cubical, perhaps sized types, perhaps something else.

[nad]

As noted by @identicalsnowflake (#2515 (comment)) there is an additional problem: when a .agdai file is loaded we don't check that the current options are consistent with those used when the file was created.

[identicalsnowflake]

There may be some logic for this already, actually, it just seems to be backwards. For example, you may have a {-# OPTIONS --safe #-} module depend on a {-# OPTIONS --type-in-type #-} and Agda will not complain; however, if you try to make a --type-in-type module depend on a --safe module, Agda will forbid it.

[nad]

I've added the "false" label, because I assume that one can currently use --cubical in one module, --with-K in another, and produce an inconsistency by combining the two.

[nad]

I guess it makes sense to fix #2783 and #2784 at the same time as (or before) this issue.

[MatthewDaggitt]

Given that this doesn't appear to be an immediate priority, an extra Known Issue should definitely be added at the bottom of the Safe Agda documentation, saying you currently need to delete all .agdai files before running agda --safe. As #3029 shows, this is still tripping myself and other people up.

[nad]

--guardedness and --sized-types do not have to be inconsistent with each other, as opposed to e.g. univalence and --with-K. We want to eventually fix the bugs that make them so.

@fredrikNordvallForsberg stated that his current implementation activates both when --safe is not used, but deactivates both when --safe is used. Does this sound reasonable to you?

Apparently the implementation also allows --safe --sized-types.

[Saizan]

@nad that sounds reasonable, yes.

[nad]

Thanks!