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

[Nils Anders Danielsson]

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.
Consider the following code:

   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 = cong proj irr

As it happens the last definition does not type check, so perhaps we
cannot use this bug to produce an inconsistency, but it is at least
clear that the type system is broken in some way.

-- 
/NAD