[Agda] ANNOUNCE: Agda 2.2.10

[Jean-Philippe Bernardy]

>> 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.

That does not really convince me of the incorrectness of the definition.
(after all b could be irrelevant for _==_ as well... :).
Can you construct a an example where such a data type really breaks the
system (for example in a way that makes computation fail)?

> What is happening here is that the index b was erased (printed as _).

Is an irrelevant argument erased as soon as it is type-checked?

> But two erased things have not necessarily been equal.

It seemed to me that, on the contrary, a major advantage of irrelevance
were that erased things were always equal, and that proofs of their
equality were always trivial.

See for example the beautiful:
http://web.student.chalmers.se/~stevan/ctfp/html/Category.Opposite.html

Help :)
-- JP