Issue2897.agda:17,12-14
Named where-modules are not allowed when module parameters have
been refined by pattern matching. See
https://github.com/agda/agda/issues/2897.
In this case the module parameters have been refined to
  n = 0
when checking the named where block M'
