[Agda] question about instance arguments

[Peter Selinger]

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