[Agda] missed termination failure

[Guillaume Brunerie]

Hi Sergei,

This does look like a bug.
I simplified the code and reported it at
https://github.com/agda/agda/issues/4165)

Best regards,
Guillaume

Den ons 30 okt. 2019 kl 21:58 skrev <mechvel at scico.botik.ru>:
>
> I have an impression that the attached M.agda has been deleted by some
> filter,
> due to a problem with UTF symbols.
> (?)
>
> So I attach now  M.agda.zip.
>
> --
> SM
>
>
> On 2019-10-28 16:29, mechvel at scico.botik.ru wrote:
> > Dear Agda developers,
> >
> > I wonder of whether the attached program presents a bug in the type
> > checker of  2.6.0.1.
> > The program is small.
> > Its last line has
> >               [y] = [y]          -- DEBUG
> > instead of    [y] = [ y ]
> >
> > The second version is type-checked fast.
> > The first version probably needs a report like "Termination check
> > failed",
> > but it hangs for a very long time.
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > 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