Agda-2.3.2.2: test/fail/ShapeIrrelevantIndexNoBecauseOfRecursion.err

ShapeIrrelevantIndexNoBecauseOfRecursion.agda:26,14-15
.a != .b of type Bool
when checking that the expression x has type D .b