[Agda] question about instance arguments

[Andreas Abel]

I quickly updated the reference manual (inserted the "instance" keyword 
in the example).  Someone might do it properly...

On 04.12.2014 10:14, Dominique Devriese wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/