[Agda] change in handling of irrelevant parameters (bug?)

[Darin Morrison]

Hi All,

I noticed a change in the handling of irrelevant parameters between 2.2.9 and 2.2.10 which I think is beyond having irrelevant projections enabled by default.  Code like the following seems to be rejected by 2.2.9 but not 2.2.10:

module M where

data T (A : Set) : Set where
  c : .A → T A

d : ∀ {A} → T A → A
d (c x) = x

Is this the intended behaviour or a bug?

Sorry if this has been covered before already.  I searched the mailing list but didn't find anything.

Regards,
Darin