errors/NotAModuleExpr.agda:5,1-21
The right-hand side of a module definition must have the form 'M e1
.. en' where M is a module name. The expression \x -> x doesn't.
when scope checking the declaration
  module Bad = \x -> x