[Agda] instance candidates in record fields

[Andreas Abel]

I am actually fixing this, so your code should work with the latest 
development version.  (Try it again tomorrow!)

Cheers, Andreas

On 27.07.2016 20:15, Andreas Abel wrote:
> 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/