Agda-2.3.2.2: test/fail/Issue610.err
Issue610.agda:22,9-17 Identifier R.helper is declared irrelevant, so it cannot be used here when checking that the expression R.helper x x has type Set
Issue610.agda:22,9-17 Identifier R.helper is declared irrelevant, so it cannot be used here when checking that the expression R.helper x x has type Set