record R : Set₁ where
  X = Y  -- should get error here
  field A : Set