Compiling the following code

type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where
  R x y Refl = Refl

fails with the error

Temp.hs:49:9: error:
    • Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’
    • In the third argument of ‘R’, namely ‘Refl’
      In the type family declaration for ‘R’
   |
49 |   R x y Refl = Refl
   |         ^^^^

where Refl is defined as

data a :~: b where
  Refl :: a :~: a

I would expect pattern-matching on Refl to bring the equality x ~ y into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.

(both 8.2.2 and HEAD)