[Agda] Irrelevance + instance arguments = inconsistency in 2.3.0

[Nils Anders Danielsson]

On 2012-01-11 13:17, 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. See the
> attached file for details. The crucial part is that a (relevant)
> instance argument will be automatically filled in by an irrelevant value
> in the context, even though that value would be (correctly) rejected
> when given explicitly.

Please report this issue on the bug tracker.

I suspect that this problem would have been avoided if Agda had had a
small trusted core (which did not include instance arguments).

-- 
/NAD