[Agda] question on `Any'

[Sergei Meshveliani]

Please, why is not this type-checked  
(for  A : Setoid c l;  C = Carrier A)
?
  open Any   
  f : (x : C) → (ys : List C) → Any (_≈_ x) ys → List C
  f x _  (here _) = []
  f x ys _        = []

The report is
----------------
x₁ ∷ xs != ys of type 
List (...Carrier ...)
when checking that the pattern here _ has type Any (_≈_ x) ys
----------------

And commenting out the line of  `here'  makes the rest checked.
Is Agda correct in these examples? 

Thanks,

------
Sergei