Safe Agda¶
By using the command-line option --safe
, 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
allows the user to encode the Girard-Hurken paradox.--injective-type-constructors
together with excluded middle leads to an inconsistency via Chnug-Kil Hur’s construction.guardedness-preserving-type-constructors
is based on a rather operational understanding of∞
/♯_
; it’s not yet clear if this extension is consistent.--experimental-irrelevance
enables potentially unsound irrelevance features (irrelevant levels, irrelevant data matching).--rewriting
turns any equation into one that holds definitionally. It can at the very least break convergence.
Known Issues¶
Pragma Option¶
It is possible to specify {-# OPTIONS --safe #-}
at the top of a file.
Unfortunately a known bug (see #2487)
means that the option choice is not repercuted in the imported file. Therefore
only the command-line option can be trusted.
Standard Library¶
The standard library uses a lot of unsafe features (e.g. postulate
in
the Foreign Function Interface) and these are not isolated in separate
modules. As a consequence virtually any project relying on the standard
library will not be successfully typechecked with the --safe
option.
There is work in progress
to fix this issue.