Safe Agda

By using the option --safe (as a pragma option, or on the command-line), a user can specify that Agda should ensure that features leading to possible inconsistencies should be disabled.

Here is a list of the features --safe is incompatible with:

The option --safe is coinfective (see Checking options for consistency); if a module is declared safe, then all its imported modules must also be declared safe.