UselessPrivateImport2.agda:3,1-4,52 Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations.