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