Reputation: 3218
I'm trying to follow the code for McBride's How to Keep Your Neighbours in Order, and can't understand why Agda (I'm using Agda 2.4.2.2) gives the following error message:
Instance search can only be used to find elements in a named type when checking that the expression
t
has type.T
for function _:-_
. The code is given bellow
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
Any help is highly appreciated.
Upvotes: 3
Views: 345
Reputation: 12735
There was a recent email by Nils Anders Danielsson at the agda-dev mailing list precisely about this. I cannot find it online, so here is a quote:
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
Upvotes: 4