-- Useless private module Issue476a where A : Set₁ private A = Set