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
; forces Agda to accept unfinished proofs.--no-positivity-check
; makes it possible to write non-terminating programs by structural “induction” on non strictly positive datatypes.--no-termination-check
; gives loopy programs any type.--type-in-type
and--omega-in-omega
; allow the user to encode the Girard-Hurken paradox.--injective-type-constructors
; together with excluded middle leads to an inconsistency via Chung-Kil Hur’s construction.--sized-types
; lacks some checks that rule out improper, inconsistent uses of sizes.--experimental-irrelevance
and--irrelevant-projections
; enables potentially unsound irrelevance features (irrelevant levels, irrelevant data matching, and projection of irrelevant record fields, respectively).--rewriting
; turns any equation into one that holds definitionally. It can at the very least break convergence.--cubical-compatible
together with--with-K
; the univalence axiom is provable using cubical constructions, which falsifies the K axiom.--without-K
together with--flat-split
The
primEraseEquality
primitive together with--without-K
; usingprimEraseEquality
, one can derive 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.
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.