module Issue580 where record Bad : Set₁ where private field A : Set