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

[effectfully]

See here https://lists.chalmers.se/pipermail/agda-dev/2015-January/000048.html

2015-10-23 5:38 GMT+03:00, Martin Stone Davis <martin.stone.davis at gmail.com>:
> 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
>