Issue719.agda:6,23-24 Duplicate definition of module A. Previous definition of module A at Size.agda:7,15-19 when scope checking the declaration open module A = M