[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