Agda-2.3.2.2: test/fail/IrrelevantModuleParameter.agda

module IrrelevantModuleParameter .(A : Set) where

postulate 
  a : A
-- cannot declare something of type A, since A is irrelevant