errors/NoSuchModule.agda:3,1-7
No such module X
when scope checking the declaration
  open X