[Agda] instance candidates in record fields

Guillermo Calderon calderon at fing.edu.uy
Thu Jul 21 21:04:12 CEST 2016


Hi;

I have a problem working with instance arguments in Agda 2.5.1

Here is a simplified code to illustrate the problem:

----------------------------------------------
-- my class
record MyClass  : Set₁ where
   field
    C  : Set
    op : C → C → C
    eq : C → C → Set

-- a record using MyClass
record Q (CA CB : MyClass) : Set where

   open MyClass ⦃...⦄
   instance fooA = CA
            fooB = CB

   A = MyClass.C CA
   B = MyClass.C CB

  field
     f : A → B
     prop : ∀ {a b} → eq a b → eq (f a) (f b)
               ^^^    ^^^^^^
                (yellow)
-----------------------------------------------

Agda gives this message:  "No instance of type MyClass was found in 
scope. ...".

I can fix it  declaring the instances fooA and fooB local to prop (using 
a let).  Other solution is to use {{ }} for parameters CA y CB.
However, I think that the code above should work.
Why it doesn't?

Thanks in advance
Guillermo



More information about the Agda mailing list