Agda-2.3.2.2: test/fail/IrrelevantRecordMatching.err
IrrelevantRecordMatching.agda:12,22-23 Variable a is declared irrelevant, so it cannot be used here when checking that the expression a has type .A
IrrelevantRecordMatching.agda:12,22-23 Variable a is declared irrelevant, so it cannot be used here when checking that the expression a has type .A