[Agda] change in handling of irrelevant parameters (bug?)

[Darin Morrison]

On 15 Mar 2011, at 12:35, Nils Anders Danielsson wrote:

> On 2011-03-15 12:02, Darin Morrison wrote:
>> I noticed a change in the handling of irrelevant parameters between
>> 2.2.9 and 2.2.10 which I think is beyond having irrelevant projections
>> enabled by default. [...]
> 
> I don't know too much about irrelevance, but this doesn't look good.

From the 2.2.8 release notes, it says:

>     Irrelevant arguments can only be used in irrelevant contexts.
>     Consider the following subset type:
> 
>       data Subset (A : Set) (P : A → Set) : Set where
>         _#_ : (elem : A) → .(P elem) → Subset A P
> 
>     The following two uses are fine:
> 
>       elimSubset : ∀ {A C : Set} {P} →
>                    Subset A P → ((a : A) → .(P a) → C) → C
>       elimSubset (a # p) k = k a p
> 
>       elem : {A : Set} {P : A → Set} → Subset A P → A
>       elem (x # p) = x
> 
>     However, if we try to project out the proof component, then Agda
>     complains that “variable p is declared irrelevant, so it cannot be
>     used here”:
> 
>       prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
>       prjProof (a # p) = p

This restriction to using irrelevant arguments in irrelevant contexts is what I would expect and that is what seems to have been changed in the most recent release.

However, in the 2.2.10 release notes, it states the following:

>    Postulates and functions can be marked as irrelevant by prefixing
>    the name with a dot when the name is declared. Example:
> 
>      postulate
>        .irrelevant : {A : Set} → .A → A
> 
>    Irrelevant names may only be used in irrelevant positions or in
>    definitions of things which have been declared irrelevant.
> 
>    The axiom irrelevant above can be used to define a projection from
>    an irrelevant record field:
> 
>      data Subset (A : Set) (P : A → Set) : Set where
>        _#_ : (a : A) → .(P a) → Subset A P
> 
>      elem : ∀ {A P} → Subset A P → A
>      elem (a # p) = a
> 
>      .certificate : ∀ {A P} (x : Subset A P) → P (elem x)
>      certificate (a # p) = irrelevant p
> 
>    The right-hand side of certificate is relevant, so we cannot define
> 
>      certificate (a # p) = p
> 
>    (because p is irrelevant). However, certificate is declared to be
>    irrelevant, so it can use the axiom irrelevant. Furthermore the
>    first argument of the axiom is irrelevant, which means that
>    irrelevant p is well-formed.

This makes me think that in the code you posted, 'proj' should have to be marked as irrelevant to typecheck, e.g.,

  data Bool : Set where
    true : Bool
    false : Bool

  data _≡_ {A} (x : A) : A → Set where
    refl : x ≡ x

  resp : ∀ {A₁ A₂ x₁ x₂} (f : A₁ → A₂) → x₁ ≡ x₂ → f x₁ ≡ f x₂
  resp f refl = refl

  data D : Set where
    c : .Bool → D

  irr : c true ≡ c false
  irr = refl

  .proj : D → Bool
  proj (c x) = x

  bad : proj (c true) ≡ proj (c false)
  bad = resp proj irr

In this case, 'bad' would fail to type check for a more expected reason, namely that 'proj' is being used in a non-relevant position.

So maybe the problem is just that the condition mentioned in the 2.2.10 release notes is not properly enforced?

This is pretty important for me as I have a large development that relies on irrelevant fields quite heavily.  Without them, the code type-checks far too slowly to be usable.  I don't think I'm unintentionally relying on bugs in the implementation in my proofs but now I'm a little bit worried...

Cheers,
Darin