[Agda] ANNOUNCE: Agda 2.2.10

[Andreas Abel]

On 2/22/11 4:12 PM, Jean-Philippe Bernardy wrote:
> On Sun, Feb 20, 2011 at 7:23 PM, Nils Anders Danielsson<nad at chalmers.se>  wrote:
>
>> * Irrelevant declarations.
>
> I tried to define:
>
> data Eq (A : Set) (a : A) : .A ->  Set where
>    refl : Eq A a a

This should be rejected by Agda, so this is where the bug is located. 
If you spell this out it means

   data Eq A a .b : Set where
     refl : a == b -> Eq A a b

but b is declared irrelevant.  I will have to revisit irrelevant family 
indices!

> but:
>
> subst : ∀ A a b ->  (P : A ->  Set) ->  Eq A a b ->  P a ->  P b
> subst A a .a p refl = ?
>
> gives the rather unhelpful message:
>
> _ != _ of type A
> when checking that the pattern refl has type Eq A a _
>
> Can somebody offer insight to what is going on?

What is happening here is that the index b was erased (printed as _). 
But two erased things have not necessarily been equal.

The bug described above lets erased things surface, which should not happen.

Cheers,
Andreas