[Agda] Why is this non-terminating?

[James Wood]

Okay, then probably this is the relevant issue:
https://github.com/agda/agda/issues/59 .
I know there have been a lot of changes to termination checking
involving `with`, because it seems very hard to do it right.

James

On 03/07/2020 21:15, Jinwoo Lee wrote:
> 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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     > https://lists.chalmers.se/mailman/listinfo/agda
>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C4f365c61233648cdb19908d81f8dcf78%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637294041217222770&sdata=H%2F4JOPhYGSztEDgluBSSeZgT8IOkLk6s7EmSFCkyJ78%3D&reserved=0>
>     >
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C4f365c61233648cdb19908d81f8dcf78%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637294041217222770&sdata=H%2F4JOPhYGSztEDgluBSSeZgT8IOkLk6s7EmSFCkyJ78%3D&reserved=0>
>