headEq with and without view refined pattern matching

heaEq.idr

-- works nicely.
headEq'' : DecEq a => (x : a) -> (ys : List a) -> NonEmpty ys -> Dec (x = head ys)
headEq'' x (y :: ys) IsNonEmpty =
   -- just return the result of `decEq`
   decEq x y

-- see:
headEq'' 1 [1, 2] : NonEmpty [1, 2] -> Dec (1 = 1)

-- what about just pattern matching on the result
-- of deqEq with `match`, and simply returning it?

headEq''' : DecEq a => (x : a) -> (ys : List a) -> NonEmpty ys -> Dec (x = head ys)
headEq''' x (y :: ys) IsNonEmpty with (decEq x y)
   -- pattern match on the result of `decEq`,
   -- then just return that value.
   | (Yes Refl) = Yes Refl
   | (No contra) = No (\Refl => contra Refl)

The error:

{-
When checking argument prf to constructor Prelude.Basics.Yes:
             Type mismatch between
                     y = y (Type of Refl)
             and
                     x = y (Expected type)
             
             Specifically:
                     Type mismatch between
                             y
                     and
                             x
-}