Problems with instance arguments in Agda

Question

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.

user3237465 user3237465 · Accepted Answer · 2015-03-13T01:07:43

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

Problems with instance arguments in Agda

1 Answers