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.--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.--guardedness
together with--sized-types
; currently can be used to define a type which is both inductive and coinductive, which leads to an inconsistency. This might be fixed in the future.--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
together with--with-K
; the univalence axiom is provable using cubical constructions, which falsifies the K axiom.- The
primEraseEquality
primitive together with--without-K
; usingprimEraseEquality
, one can derive the K axiom.
The option --safe
is coinfective (see
Consistency checking of options used); if a module is declared safe,
then all its imported modules must also be declared safe.
Note
The --guardedness
and --sized-types
options are both on by default.
However, unless they have been set explicitly by the user, setting the
--safe
option will turn them both off. That is to say that
{-# OPTIONS --safe #-}
will correspond to --safe
, --no-guardedness
, and --no-sized-types
.
When both
{-# OPTIONS --safe --guardedness #-}
and
{-# OPTIONS --guardedness --safe #-}
will turn on --safe
, --guardedness
, and --no-sized-types
.
Setting both --sized-types
and --guardedness
whilst demanding that the
module is --safe
will lead to an error as combining these options currently
is inconsistent.