Issue473a.agda:26,7-8
d != R.f r of type D
when checking that the pattern p has type P (R.f r)