[Agda] Why is this non-terminating?

[Jinwoo Lee]

I have a function that I believe terminates but Agda disagrees.

hasDoubleLetter : List Char → Bool
hasDoubleLetter [] = false
hasDoubleLetter (c₁ ∷ cs@(c₂ ∷ _)) with c₁ == c₂
... | yes _ = true
... | no  _ = hasDoubleLetter cs    -- This is problematic.
hasDoubleLetter (_ ∷ []) = false

Because `hasDoubleLetter` is recursively applied to a "smaller" structure
(cs), I think it should be considered terminating. Am I missing something?

FWIW the error message is like below.

Termination checking failed for the following functions:
  hasDoubleLetter
Problematic calls:
  hasDoubleLetter (c₁ ∷ c₂ ∷ xs) | (EqChar Eq.== c₁) c₂
  hasDoubleLetter (c₂ ∷ xs)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200703/2578cf83/attachment.html>