Agda-2.3.2.2: test/fail/Issue87.err
Issue87.agda:9,1-10,34
Inaccessible (dotted) patterns from the parent clause must also be
inaccessible in the with clause, when checking the pattern {i},
when checking that the clause
bar (d x) (d y) with y
bar (d x) (d {i} y) | z = d {i} y
has type {i : I} → D i → D i → D i