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:

  • postulate; can be used to assume any axiom.

  • --allow-unsolved-metas; forces Agda to accept unfinished proofs.

  • --allow-incomplete-matches and pragma NON_COVERING; allows to prove false using a partial function or through a partial proof.

  • --no-positivity-check and pragmas NO_POSITIVITY_CHECK and POLARITY; make it possible to write non-terminating programs via datatypes that are not strictly positive.

  • --no-termination-check and pragmas TERMINATING and NON_TERMINATING; give loopy programs any type.

  • --type-in-type and --omega-in-omega and pragma NO_UNIVERSE_CHECK; allow the user to encode the Girard-Hurken paradox.

  • pragma INJECTIVE; allows to prove false by declaring a non-injective function as injective.

  • pragma ETA; can be used force eta-equality for unguarded recursive records which can make Agda loop.

  • --cubical=compatible together with --with-K; the univalence axiom is provable using cubical constructions, which falsifies the K axiom.

  • --allow-exec; allows system calls during type checking.

  • --no-load-primitives; allows the user to bind the sort and level primitives manually.

  • --cumulativity; due to its poor heuristic for solving universe levels.

  • --large-indices together with --without-K or --forced-argument-recursion; both of these combinations are known to be inconsistent.

  • pragma COMPILE; allows to change the meaning of code during compilation.

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.