Irrelevance bug to prove false

[GoogleCodeExporter]

When we were fooling around with irrelevance in #agda today, James Deikun found
that if you name your where modules in irrelevant contexts, you can make that
which is irrelevant relevant again, with some other trickery:

module RelevanceBug where

open import Level
open import Relation.Binary.PropositionalEquality

open import Data.Empty
open import Data.Unit

record A : Set₁ where
  constructor set
  field
    .a : Set

.get : A → Set
get x = helper x
  module R where
  helper : .A -> Set
  helper x = A.a x

ack : A → Set
ack x = R.helper x x

hah : set ⊤ ≡ set ⊥
hah = refl

.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo

An odd aspect to this hack is that cong ack hah does not have type ⊤ ≡ ⊥,
but rather has type .(⊤) ≡ .(⊥) which is actually considered distinct and
won't unify. Luckily, in the irrelevant moo function above, .(⊤) ≡ .(⊥)
magically turns into ⊤ ≡ ⊥ again, and we can do great evil again.

Original issue reported on code.google.com by pumpkingod@gmail.com on 16 Apr 2012 at 9:17

[GoogleCodeExporter]

Oh, and I built Agda a couple of weeks ago. I was also surprised that it didn't ask me to postulate an irrAxiom.

Original comment by pumpkingod@gmail.com on 16 Apr 2012 at 9:34

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 17 Apr 2012 at 9:13

• Changed state: Accepted
• Added labels: Priority-Critical, Type-Defect

[GoogleCodeExporter]

There's a simpler to define ack which still makes the rest work:

.ack : A → Set
ack x = A.a x

Original comment by sanzhi...@gmail.com on 17 Apr 2012 at 9:20

[GoogleCodeExporter]

Thanks for reporting these bugs. I am currently fixing the first one (modules and irrelevance), but the second one is independent (with and irrelevance).

Original comment by andreas....@gmail.com on 18 Apr 2012 at 12:15

[GoogleCodeExporter]

Fixed.

The irrAxiom is now in the Kernel and printed as .(_)
In with functions it got lost, this is fixed now, so the great evil is cured.
Cheers, Andreas

Original comment by andreas....@gmail.com on 18 Apr 2012 at 1:08

• Changed state: Fixed
• Added labels: Irrelevance, With

[Saizan]

Sometimes they come back:

open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality

data A : Set₁ where
  set : .Set -> A

module M .(x : Set) where

  .out : Set
  out = x

.ack : A → Set
ack (set x) = M.out x

hah : set ⊤ ≡ set ⊥
hah = refl

.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo

[jespercockx]

I guess we'll have to reset the counter again. Note that this time, it isn't necessary to use with:

.moo : ⊥
moo = subst (λ x → x) (cong ack hah) tt

Is the application cong ack supposed to typecheck?

[UlfNorell]

I suspect that the problem is out. Note that if you try

.out : .(x : Set) → Set
out x = x

you get an error. Although I have to admit I'm not exactly sure what the rules are for irrelevant definitions.

[andreasabel]

I'm not either. But it feels like the bodies of irrelevant definitions have to be protected by a DontCare just as for irrelevant projections. It fixes this issue. The rationale is that adding a DontCare does no harm, as irrelevant terms are all equal in irrelevant context. But the DontCare prevents us from tracelessly reducing away the constructor set whose argument is irrelevant.

[andreasabel]

Associated commits (2012):

• f300ed7

Date:   Wed Apr 18 12:37:48 2012 +0000

    Declaration in irrelevant context (e.g. where modules) must be irrelevant as well.
    Fixes part of issue 610.

• 7c04157

Date:   Wed Apr 18 12:58:52 2012 +0000

    When checking a DontCare term, keep DontCare. (Fixes Issue 610-4).