{-# OPTIONS --no-irrelevant-projections #-}

module ScopeIrrelevantRecordField where

record Bla : Set1 where
  constructor mkBla
  field
    .bla0 bla1 .{bla2 bla3} {bla4 .bla5} : Set

bla0' : Bla -> Set
bla0' = Bla.bla0

-- WAS: should fail with bla0 not in scope
-- NOW: should complain about irrelevant projection
