Agda-2.3.2.2: test/fail/RecordConstructorOutOfScope.agda

module RecordConstructorOutOfScope where

record R : Set where
  constructor con

  id : R
  id = con