Agda-2.3.2.2: test/fail/ShapeIrrelevantParameterNoBecauseOfRecursion.err
ShapeIrrelevantParameterNoBecauseOfRecursion.agda:15,12-13 Variable b is declared irrelevant, so it cannot be used here when checking that the expression b has type Bool
ShapeIrrelevantParameterNoBecauseOfRecursion.agda:15,12-13 Variable b is declared irrelevant, so it cannot be used here when checking that the expression b has type Bool