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