[Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda

[Martin Stone Davis]

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 2.4.2.4:

_:-_ : forall {P T} -> <P P P> -> (P => T) -> T
> ! :- t = t
>

The error is:

Instance search can only be used to find elements in a named type
> when checking that the expression t has type .T
>

The complete source can be found in
https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda; the
particular definition at line 266. In case it helps, I've made a copy here
<http://lpaste.net/143668>.
--
Martin Stone Davis
ps
Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151022/23acdc80/attachment.html