Agda-2.3.2.2: test/fail/IrrelevantVar.err
IrrelevantVar.agda:8,9-10 Variable x is declared irrelevant, so it cannot be used here when checking that the expression x has type .A
IrrelevantVar.agda:8,9-10 Variable x is declared irrelevant, so it cannot be used here when checking that the expression x has type .A