[Agda] Irrelevance + instance arguments = inconsistency in 2.3.0

[Andreas Abel]

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/