[Agda] question about instance arguments

[Dominique Devriese]

Peter,

Firstly, the problem you're having is a result of the changes to
instance argument semantics that have been made in Agda 2.4.2, which
are not yet reflected in the reference manual and some of the error
messages.  You can look at

https://github.com/agda/agda/blob/2.4.2.2/CHANGELOG

(look for "Instance search") to see what has been changed.

2014-12-04 2:28 GMT+01:00 Peter Selinger <selinger at mathstat.dal.ca>:
> I'm trying to learn to use instance arguments, and I tried a first
> example, essentially taken from the reference manual:
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments
>
> Unfortunately, I cannot get it to work. Probably I am overlooking
> something terribly simple. I am using Agda version 2.4.2.2, freshly
> installed via Cabal.

Yes, the reference manual needs updating.

> Here's my file:
>
> module EqTest where
>
>   data Bool : Set where
>     true : Bool
>     false : Bool
>
>   eq : Bool -> Bool -> Bool
>   eq true true = true
>   eq false false = true
>   eq _ _ = false
>
>   record Eq (t : Set) : Set where
>     field
>       _==_ : t -> t -> Bool
>
>   open Eq {{...}}
>
>   eqBool : Eq Bool
>   eqBool = record { _==_ = eq }

Essentially, you need to change this to
   instance eqBool : Eq Bool
   eqBool = record { _==_ = eq }

>   test1 = true == true

> The error message I receive, in the test1 line, is:
>
> /home/selinger/projects/lang/agda/EqTest.agda:21,16-18
> No variable of type Eq Bool was found in scope.
> when checking that true true are valid arguments to a function of
> type {t : Set} {{r : Eq t}} → t → t → Bool
>
> This seems contradictory, since the variable eqBool is indeed in
> scope.

It would probably be a good idea to change this error message to
something like "... was found using the instances in scope"?

> If I replace the eqBool definition by a postulate, as in the
> reference manual,
>
>   postulate eqBool : Eq Bool
>
> I get the same error message.

Yes, this makes no difference.

> On the other hand, if I write
>
>   test1 = let e = eqBool in true == true
>
> the error disappears in both cases.

Ah, this surprises me, I thought you had to annotate let-bound
variables as well using instance under the new schem.

> On the other hand, this does not
> work:
>
>   test1 = true == true
>     where e = eqBool

This is expected under the new semantics.

> The reference manual says:
>
> "A candidate expression is any identifier (possibly applied to a
> hidden argument) in scope (either imported or defined previously in
> the file) or in the context (e.g. section arguments or arguments of
> the current function)."
>
> My example seems to contradict that. Is it a bug?

Yes, it is a bug in the reference manual :).  It should be updated to
reflect the new semantics.

Dominique