WithoutK8.agda:20,1-7
The indices
  M.d
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the clause Foo () has type P d → Set