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