Agda-2.3.2.2: test/fail/ScopeIrrelevantRecordField.err

ScopeIrrelevantRecordField.agda:10,9-17
Not in scope:
  Bla.bla0
  at ScopeIrrelevantRecordField.agda:10,9-17
when scope checking Bla.bla0