packages feed

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