[Agda] matching to Sum

[Sergei Meshveliani]

Please, why the pattern  (inj₁ y∈xs)   below is checked-out?

I know that 
       cons-hasRepetition A x xs hasRep-xs =  inj₂ hasRep-xs

is sufficient. 
But the question about the pattern  (inj₁ y∈xs)  still remains.


-----------------------------------------------------------------
module Report4 where
open import Level using (Level; _⊔_; Lift)
open import Relation.Binary using (Setoid; module Setoid)
open import Data.Empty    using (⊥)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.List     using (List; []; _∷_)
open import Data.List.Any using (module Membership)

--------------------------------------------------------------------            
hasRepetition : ∀ {c l} (A : Setoid c l) → List (Setoid.Carrier A) →
                                                        Set (c ⊔ l)
hasRepetition _ []       =  Lift ⊥
hasRepetition A (x ∷ xs) =  x ∈ xs  ⊎ (hasRepetition A xs)
                        where
                        open module MembA = Membership A using (_∈_)

cons-hasRepetition :
        ∀ {c l} (A : Setoid c l) →
        let C = Setoid.Carrier A
        in
        (x : C) → (xs : List C) → hasRepetition A xs → 
                                  hasRepetition A (x ∷ xs)

cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) =  inj₂ (inj₁ y∈xs)
--------------------------------------------------------------------

The report is 

  Cannot split on argument of non-datatype   hasRepetition A xs
  when checking the definition of  cons-hasRepetition.


Thank you in advance for explanation,

------
Sergei