[Agda] missed termination failure

[mechvel at scico.botik.ru]

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
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: M.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191028/07d848f6/attachment.ksh>