On Saturday, September 18th, 2021 at 14:12, Anthony Clayden <anthony.d.clayden@gmail.com> wrote:

The end of your error message:

>       |
>    63 | pattern Any a <- Some a
>       |                       ^


Appears to have program text (a mono-directional pattern binding) that doesn't correspond to the program text you quote.

I just tried both ways of writing bidirectional pattern synonmys, neither worked with explicit `forall`.


I'm suspecting the explicit forall is not much to do with it.


With an implicit forall, the code does type check.

Regards,
Marcin