[Agda] bug?

[mechvel at scico.botik.ru]

Dear Agda developers,

I am testing  lib-1.4-rc1

under Agda 2.6.1, ghc-8.8.3, Ubuntu Linux 18.04.

Many modules in my large application have been ported.
But the current module is not type-checked.
I have composed of this a self-contained and small code

- which is attached.

Probably the type checker is responsible.
Less probably this is of  lib-1.4-rc1.
And I doubt whether something is wrong in the program itself.

   > agda $agdaLibOpt Bug.agda

reports a strange thing for the last line of the attached program:

"
Checking Bug (/home/mechvel/agda/toSave/bugs/sept1-2020/Bug.agda).
/home/mechvel/agda/toSave/bugs/sept1-2020/Bug.agda:60,15-45
Refusing to invert pattern matching of Data.List.foldl because the
maximum depth (50) has been reached. Most likely this means you
have an unsatisfiable constraint, but it could also mean that you
need to increase the maximum depth using the flag
--inversion-max-depth=N
when checking that the inferred type of an application
   All (_≤ n)
   (reverse
    (_x_114 ∷
...
<a very long expression folllows>
"

I recall, this code worked under lib-1.3
(it is not for sure that it is the very same code).
There the constraint was satisfiable, and with  lib-1.4-rc1  it is not.

What might all this mean?

Thanks,

------
Sergei
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Bug.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200902/e05f2cfa/attachment.ksh>