[Agda] Matching on crisp refl leads to error

[Felix Cherubini]

Hi all,

I noticed that the latest master of agda does not accept the following:


{-# OPTIONS --cubical #-}
open import Agda.Primitive

data ♭ (@♭ A : Set) : Set where
     _^♭ : (@♭ a : A) → ♭ A

data _≡'_ {A : Set} : A → A → Set where
   refl' : {x : A} → x ≡' x

♭≡'→≡'♭ : {@♭ A : Set} {@♭ u v : A} → ♭ (u ≡' v) → (u ^♭) ≡' (v ^♭)
♭≡'→≡'♭ (refl' ^♭) = refl'


With the error message:


/home/felix/FindBug2.agda:11,1-27
Agda.Primitive.Cubical.primTransp
(λ i →
    (u ^♭) ≡'
    (Agda.Primitive.Cubical.primTransp
     (λ i₁ → Agda.Primitive.Cubical.PathP (λ i₂ → A) (x i₁) u) φ x₁
     (Agda.Primitive.Cubical.primINeg i)
     ^♭))
φ (♭≡'→≡'♭ (refl' ^♭)) is not usable at the required modality .
when checking the definition of ♭≡'→≡'♭


Is it a bug or intentional?
The same code checked in Agda 2.6.2.2 and 2.6.2. Matching in the same 
way on constructors of non-dependent inductive types is accepted.

All the best,

Felix