<div dir="ltr"><div>Would someone help me get Conor's McBride's code to typecheck? I'm trying to follow "How to keep your Neighbours in Order", 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} -> <P P P> -> (P => T) -> 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'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>