Agda-2.3.2.2: test/fail/Issue719.agda

module Issue719 where

  import Common.Size as A
  module M where

  private open module A = M

-- NOT NICE:
-- Duplicate definition of module A. Previous definition of module A
-- at /Users/abel/cover/alfa/Agda2-clean/test/Common/Size.agda:7,15-19
-- when scope checking the declaration
--   open module A = M