IrrelevantModuleParameter1.err

IrrelevantModuleParameter1.agda:5,9-10
Variable a is declared irrelevant, so it cannot be used here
when checking that the expression a has type A