Agda-2.3.2.2: test/fail/Issue292d.err
Issue292d.agda:33,1-13 Cannot decide whether there should be a case for the constructor d₂, since the unification gets stuck on unifying the inferred indices [i₂] with the expected indices [i₁] when checking the definition of Bad