[Agda] record field ambiguity

[Nils Anders Danielsson]

On 2013-05-09 13:07, Sergei Meshveliani wrote:
> Can you, please, explain the checker behavior
>                                       (Agda-2.3.2, MAlonzo, lib-0.7)
> in the below program?
>
>
> (1) M.ResidueLI  is a record parameterized by  (I : DReductionLIdeal);
>      the function  residueSetoid  takes  rdI : DReductionLIdeal
>      and uses
>      rCarr = M.ResidueLI rdI    as a carrier for operations.
>
> But I need to use  Res-rdI = M.ResidueLI rdI
>
> as a module, with the value  rdI  instantiated, and use the field value
> resRepr  of  Res-rdI.
>
> And my attempts with  module Res-rdI = ResidueLI rdI,
> with                  ResidueLI.resRepr rdI,
> with                  resRepr = ResidueLI.resRepr rCarr
>
> -- are rejected, because the checker requires for  rdI  some strange
> type instead of  DReductionLIdeal  declared for  rdI.

There is an explanation of record modules in Ulf's tutorial.

-- 
/NAD