[Agda] termination checking loop

[Andreas Abel]

Smaller examples are better.  I am happy to wait until after October 20.

Best,
Andreas

On 2019-09-29 20:05, mechvel at scico.botik.ru wrote:
> On 2019-09-29 20:33, Andreas Abel wrote:
>> [..]>
>> Can't judge from the information in your message.  Please provide a 
>> reproducible test case.
>> [..]
> 
> It is difficult to reduce the example. Because it is large, and needs to 
> run the type checker during
> many minutes after each step of the code change. Is there any other 
> approach possible?
> 
> (1) I can provide a large example right now, almost as it is
>      (probably it can be reduced several times).
> (2) I can try to reduce it, but this attempt can happen after about 
> October 20.
> 
> What would you choose of these two?
> 
> -- 
> SM
> 
> 
>>
>> 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
>