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