[Agda] termination checking loop

[mechvel at scico.botik.ru]

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