[Agda] question about instance arguments

[Andreas Abel]

Starting with Agda 2.4.2, you need to explicitly declare instances, so

   instance
     eqBool : Eq Bool
     ...

will (hopefully) fix your problem.

Cheers,
Andreas

On 04.12.2014 02:28, Peter Selinger wrote:
> Hi,
>
> 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.
>
> 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 }
>
>    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. If I replace the eqBool definition by a postulate, as in the
> reference manual,
>
>    postulate eqBool : Eq Bool
>
> I get the same error message. On the other hand, if I write
>
>    test1 = let e = eqBool in true == true
>
> the error disappears in both cases. On the other hand, this does not
> work:
>
>    test1 = true == true
>      where e = eqBool
>
> 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? Thanks, -- Peter
>
> _______________________________________________
> 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/