Agda-2.3.2.2: test/fail/Issue260c.agda
-- Module shadowing using generated modules for records and datatypes module Issue260c where record R : Set where module R where
-- Module shadowing using generated modules for records and datatypes module Issue260c where record R : Set where module R where