[Agda] termination checking loop

[Andreas Abel]

Dear Sergei,

Can't judge from the information in your message.  Please provide a 
reproducible test case.

Best,
Andreas

On 2019-09-29 14:57, mechvel at scico.botik.ru wrote:
> Dear Agda developers,
> 
> I have a module Foo.agda in which the last line for `foo' is erroneously 
> set of kind  x = x.
> 
> foo mon {f} nn =
>    begin-p
>      f *pm mon                       =ₚ[ =ₚsym .. (*mp-comm mon f) ]
>      mon *mp f                       =ₚ[ ... ]
>      (mon *ₘ lmF) +mp (mon *mp fₜ)   =ₚ[ ... ]
>      (lmF *ₘ mon) +mp (fₜ *pm mon)
>    ∎p
>    where
>    lmF = lm f nn;   fₜ = tailPol f nn
>    ...
>    fₜ*m = fₜ*m    -- **
> 
> And the type checker of  Agda 2.6.0.1  seems to loop infinitely (> 30 
> minutes, for large memory space).
> 
> 1) If I replace this marked clause with the needed one, then Foo.agda is 
> type-checked fast.
> 2) I tried to set a clause of kind  x = x  in several previous and 
> similar places in Foo.agda,
>     after `where` in "begin-p ... ∎p where".
>     And it type-checks fast, reporting "Termination checking failed for 
> the following functions: ...".
> 
> What might this mean?
> As I recall, when the type checker loops infinitely, it is considered as 
> a bug.
> 
> Regards,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda