[Agda] Irrelevance + instance arguments = inconsistency in 2.3.0

[Adam Gundry]

Hi all,

I realise that irrelevant record projections are inconsistent anyway
[1], but I think I've found another problem with irrelevance that
doesn't depend on them and uses instance arguments instead. See the
attached file for details. The crucial part is that a (relevant)
instance argument will be automatically filled in by an irrelevant value
in the context, even though that value would be (correctly) rejected
when given explicitly.

Apologies if this is an already known problem or I'm misunderstanding
what is going on.

Adam Gundry

[1] http://code.google.com/p/agda/issues/detail?id=543
-------------- next part --------------
module Irrelevance where

open import Data.Bool using (Bool ; true ; false)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)
open import Function using (_∘_)


implicit : {A : Set}{{a : A}} -> A
implicit {{a}} = a

-- I don't know why this doesn't just work with Bool, but requires an
-- isomorphic copy of it.

record PackBool : Set where
  constructor pack
  field unpack : Bool
open PackBool

data IrrBool : Set where
  irr : .(b : PackBool) -> IrrBool 

p : irr (pack true) ≡ irr (pack false)
p = refl

-- Everything above this comment is fine; but now we can project out
-- the irrelevant value using instance arguments:

unirr : IrrBool -> PackBool
unirr (irr x) = implicit
-- unirr (irr x) = x gives an error message (as well it should)
-- but using instance arguments circumvents the check.

q : true ≡ false
q = cong (unpack ∘ unirr) p