Agda 中实例参数的问题

我正在尝试遵循 McBride's 的代码如何维持邻居秩序 https://personal.cis.strath.ac.uk/conor.mcbride/pub/Pivotal.pdf，并且无法理解为什么 Agda （我正在使用 Agda 2.4.2.2）给出以下错误消息：

实例搜索只能用于查找命名类型中的元素 当检查表达式时t有类型.T

为了功能_:-_。代码如下

data Zero : Set where

record One : Set where
  constructor <>

data Two : Set where tt ff : Two

So : Two -> Set
So tt = One
So ff = Zero

record <<_>> (P : Set) : Set where
  constructor !
  field
    {{ prf }} : P

_=>_ : Set -> Set -> Set
P => T = {{ p : P }} -> T

infixr 3 _=>_

-- problem HERE!

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

非常感谢任何帮助。

最近，agda-dev 邮件列表中尼尔斯·安德斯·丹尼尔森 (Nils Anders Danielsson) 发了一封关于此问题的电子邮件。网上找不到，所以引用一下：

康纳在“如何让你的邻居 in Order”。但是，他的代码是使用旧版本的 实例参数，现在无法检查。我设法编写了代码 使用一些小调整再次工作，并想知道我们是否可以摆脱困境 甚至更少：

我更换了

record One : Set where constructor it

with

record One : Set where
  instance
    constructor it.

这对我来说似乎很好。

我更换了

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

with

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

因为“实例搜索只能用于查找 a 中的元素 命名类型”。类似地，在两种情况下我替换了模块参数

(L : REL P)

with

(L' : REL P) (let L = Named L'),

其中 Named 是命名类型系列：

data Named {P : Set} (A : REL P) : REL P where
  named : forall {x} -> A x -> Named A x