agda - Agda 中实例参数的问题

Question

我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 的代码，并且无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误信息:

Instance search can only be used to find elements in a named type when checking that the expression t has type .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

非常感谢任何帮助。

Answer 1

Nils Anders Danielsson 最近在 agda-dev 邮件列表中有一封电子邮件正是关于此的。我在网上找不到它，所以引用一下:

Conor uses lots of instance arguments in "How to Keep Your Neighbours in Order". However, his code was written using the old variant of the instance arguments, and fails to check now. I managed to make the code work again using some small tweaks, and wonder if we could get away with even less:

I replaced

record One : Set where constructor it

with

record One : Set where
  instance
    constructor it.

This seems fine with me.

I replaced

_:-_ : 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}},

because "Instance search can only be used to find elements in a named type". Similarly, in two cases I replaced a module parameter

(L : REL P)

with

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

where Named is a named type family:

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