[Agda] Irrelevance + instance arguments = inconsistency in 2.3.0

[Andreas Abel]

This should be fixed on the darcs version (2.3.1) now.  Can you please 
verify?

Thanks,
Andreas

On 1/11/12 3:40 PM, Andreas Abel wrote:
> Hello Adam,
>
> Thanks for filing the report!
>
> On 1/11/12 1:17 PM, Adam Gundry wrote:
>> 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.
>
> The problem you describe is independent from irrelevant record
> projections, since you do not use any.
>
> Instance search does not respect irrelevance, this is why you can derive
> a contradiction. However, that should be easily fixable.
>
> 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/