[Agda] Why is this non-terminating?

[Jinwoo Lee]

Thanks, James. Removing the @-pattern didn't affect anything. But replacing
`with` with `if_then_else_` fixes it. Seems like a compiler bug.

Cheers


On Fri, Jul 3, 2020 at 1:07 PM James Wood <james.wood.100 at strath.ac.uk>
wrote:

> Hi Jinwoo,
>
> It looks fine to me, so this is probably some sort of bug / lack of
> feature. Some easy things to test would be:
>
> 1. Remove the @-pattern, so the pattern is `(c₁ ∷ c₂ ∷ cs)`, and the
> recursive call is on `c₂ ∷ cs`.
> 2. Remove the `with`, and instead find a way to go via `if_then_else_`.
>
> Best,
> James
>
> On 03/07/2020 20:57, Jinwoo Lee wrote:
> > 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)
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200703/a36701d3/attachment.html>