[Agda] instance candidates in record fields

[Andreas Abel]

Yes, that's a bug, thanks for reporting:

   https://github.com/agda/agda/issues/2117

I intend to fix it for now by outlawing instance declarations in record 
types.  However, someone should sit down and rethink type-checking of 
record declarations.

On 21.07.2016 21:04, Guillermo Calderon wrote:
>
> 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)


-- 
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/