[Agda] simple with->case fail

[mechvel at scico.botik.ru]

People,
I have

  f :  ∀ x → ¬ AnyRepeats (gfilter toSubsetIf (x ∷ []))
  f x  with member? x
  ...  | yes _ = noRepetition[x]
  ...  | no _  = noRepetition[]

which is type checked in  Agda 2.4.2.3.
But its `case' version

  f x = case member? x of \ { (yes _) → noRepetition[x]
                            ; (no _)  → noRepetition[] }

leads to the report

   _x_170 x ∷ [] != [] of type List subC
   when checking that the expression noRepetition[] has type
   (AnyRepeats (_x_170 x ∷ []) → ⊥)

Is the first version  noRepetition[]  has the needed type,
and in the second has not.

May this be all right for the type checker?

Regards,

------
Sergei