<div><br></div><div class="protonmail_quote"><div> On Saturday, September 18th, 2021 at 14:12, Anthony Clayden <anthony.d.clayden@gmail.com> wrote:<br></div><div> <br></div><blockquote type="cite" class="protonmail_quote"><div dir="ltr"><div><span class="font" style="font-family:arial, sans-serif">The end of your error message:</span><br></div><div><span class="font" style="font-family:arial, sans-serif"></span><br></div><div><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><span class="font" style="font-family:arial, sans-serif">>       |
>    63 | pattern Any a <- Some a
>       |                       ^
</span><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><span class="font" style="font-family:arial, sans-serif"></span><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><span class="font" style="font-family:arial, sans-serif">Appears to have program text (a mono-directional pattern binding) that doesn't correspond to the program text you quot</span>e.
<br></pre></div></div></blockquote></div><div>I just tried both ways of writing bidirectional pattern synonmys, neither worked with explicit `forall`.<br><br></div><div class="protonmail_quote"><blockquote type="cite" class="protonmail_quote"><div dir="ltr"><div><div><span class="font" style="font-family:arial, sans-serif"></span><br></div><div><span class="font" style="font-family:arial, sans-serif">I'm suspecting the explicit forall is not much to do with it.</span><br></div><div><span class="font" style="font-family:arial, sans-serif"></span><br></div></div></div></blockquote></div><div><br>With an implicit forall, the code does type check.<br><br>Regards,<br>Marcin<br></div>