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