Agda-2.3.2.2: test/fail/Issue580.agda

module Issue580 where

record Bad : Set₁ where
  private field A : Set