Issue314.agda:13,9-13
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  x ≟ _y_7 (x = x)
when checking that the pattern refl has type x ≡ _y_7 (x = x)
