<div dir="ltr"><div>Would someone help me get Conor&#39;s McBride&#39;s code to typecheck? I&#39;m trying to follow &quot;How to keep your Neighbours in Order&quot;, but, unfortunately, the following definition does not work in Agda <a href="http://2.4.2.4">2.4.2.4</a>:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">_:-_ : forall {P T} -&gt; &lt;P P P&gt; -&gt; (P =&gt; T) -&gt; T<br>! :- t = t<br></blockquote><div><br></div><div>The error is:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">Instance search can only be used to find elements in a named type<br>when checking that the expression t has type .T<br></blockquote><div><br>The complete source can be found in 
<a href="https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda">https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda</a>; the 
particular definition at line 266. In case it helps, I&#39;ve made a copy <a href="http://lpaste.net/143668">here</a>.<br></div></div></div>--<br><div><div><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">Martin Stone Davis<br><div>ps<br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div></div>