[Agda] ANNOUNCE: Agda 2.2.10

[Andreas Abel]

Hi Jean-Philippe,

if your definition is accepted, it means that

   refl : Eq true true

but then also

   refl : Eq true false

because the second argument is irrelevant.

Together with subst you get inconsistency.


On 2/22/11 7:27 PM, Jean-Philippe Bernardy wrote:
>>> 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.

Well what I mean here that == is beta-eta-equality.  If b is not 
present, this equality cannot be testet.

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

Yes.  These are compile-time erased arguments, unlike Barras/Bernardo or 
Mishra-Linger, which are runtime-erased arguments.

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

More precisely, irrelevant arguments are skipped, not even enter the 
equality test.  If the erased term _ surfaces, something is already at odds.

> See for example the beautiful:
> http://web.student.chalmers.se/~stevan/ctfp/html/Category.Opposite.html
>
> Help :)
> -- JP

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/