Why is `--irrelevant-projections` unsafe in Agda?

Question

In Agda, irrelevance is an annotation which marks a parameter, record field, or definition which "will only be typechecked but never evaluated", with the consequence that irrelevant arguments and record fields are ignored when checking equality.

You can define records with irrelevant fields, e.g. this "Squash" type whose elements are definitionally equal:

record Squash {ℓ} (A : Set ℓ) : Set ℓ where
  constructor squash
  field
    .unsquash : A
open Squash

and these fields are counted in absurd patterns, e.g.

foo : Squash ⊥ → ⊥
foo ()

but by default the projection .unsquash : Squash A → A doesn't actually exist, meaning you can't directly use irrelevant fields, even in an irrelevant context!

There is an option --irrelevant-projections which adds irrelevant projections for irrelevant record fields, but it's incompatible with --safe. Being able to use an irrelevant field in an irrelevant context seems pretty innocuous, so why is --irrelevant-projections unsafe?

Answer 1

--irrelevant-projections can be used to prove the irrelevance axiom mentioned in the Agda manual:

.irrAx : ∀ {ℓ} {A : Set ℓ} → .A → A
irrAx x = unsquash (squash x)

and conversely, irrelevant projections are justified by the irrelevance axiom:

.unsquash' : ∀ {ℓ} {A : Set ℓ} → Squash A → A
unsquash' (squash x) = irrAx x

Irrelevant projections and the irrelevance axiom do not compute (so e.g. unsquash (squash x) does not reduce to x). In a previous version of Agda, irrelevant projections computed, which made them inconsistent.

According to Jespr Cockx, although irrelevant projections are no longer inconsistent, the irrelevance axiom is still non-conservative and implies some form of non-constructive choice.

For example, this function looks like a formulation of the axiom of choice:

choice : ∀ {ℓ₁ ℓ₂} {X : Set ℓ₁} {Y : X → Set ℓ₂}
       → (∀ x → Squash (Y x)) → Squash (∀ x → Y x)
choice f = squash λ x → unsquash (f x)

The introduction of a non-conservative, non-constructive axiom which does not compute by necessity is, to the best of my knowledge, why --irrelevant-projections remains unsafe despite no longer being inconsistent.

See "Why does it matter if canonicity holds for irrelevant types?" for more information on the potential implications of an irrelevant non-constructive axiom.

Anyone interested in definitional proof-irrelevance may wish to consider using Prop instead, which can be used for the same purpose as irrelevance, but without so many caveats.

Some of the information in this answer has since been included in the Agda manual.