Agda-2.3.2.2: test/fail/IrrelevantModuleParameter1.agda

module IrrelevantModuleParameter1 (A : Set) .(a : A) where

postulate 
  P : A -> Set
  p : P a
-- cannot use a here, because it is irrelevant