[Agda] record field ambiguity

[Sergei Meshveliani]

Dear all,

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.

The philosophy is that the same value  c : C  is a representative
resRepr r,
for   r : ResidueLI I  over  C,   с  is considered "modulo and ideal I",
and there are possible different  I  for the same  C.
And  C  is defined globally in the parametric module  ResidueLIPack
where  ResidueLI  is defined. 


(2) Without understanding of what is happening, I tried to continue: to
import  resRepr  without instantiating  rdI  to  ResidueLI,  
and to see further.
Then, it goes up to 
                     f x = resRepr (resI x)      -- (*),

and reports there  "unsolved metas".
Then, I use
             g : rCarr -> C
             g = resRepr

(C  is the base carrier,  rCarr  is the carrier of the  ResidueLI domain
over C),
and apply  g  instead of  resRepr  in  (*).   And it is type checked!

I worry more of the point (1), because   resRepr  needs to be taken by
this concrete parameter value  rdI,  and the checker forces me to ignore
this  rdI  value. 
And as I do not understand this, the further usage of  ResidueLI  looks 
like senseless.

But the point (2) is also interesting.

By the way, instead of             resRepr (resI x),
can one write some equivalent of   (resRepr : rCarr -> C) (resI x)
(to insert a signature in-place) ?

The full precise code is on 

    http://botik.ru/pub/local/Mechveliani/agdaNotes/rep4.zip

The modules code is small, because `postulate' is set for this purpose.

This letter is copied in   readme.agda   of this archive.  

Compilation:
       agda -c -i . -i $agdaStLib +RTS -K200m -M6G -H6G -RTS Main.agda,

where  $agdaStLib  points to Standard library.

The responsible fragment is in the end of   AlgClasses3.agda,
and looks like this: 


------------------------------------------------------------------
module IdealPack (c l : Level) (upR1 : UpRingWithOne c l)
  where
  ...
  record DReductionLIdeal : Set (setoidLevel c l)
    where
    field  upLeftIdeal : UpLeftIdeal
    ...

  record ResidueLI (I : DReductionLIdeal) : Set (setoidLevel c l)
    where
    constructor resI

    field  preRepr : C

    dReductionIdeal = I
    open DReductionLIdeal I

    private reduction = reductionByGens

    open ReductionByLIdealGens reduction
                            using (in-I) renaming (genRemainder to gRem)
    resRepr : C
    resRepr = gRem preRepr


module ResidueLIPack (c l : Level) (upR1 : UpRingWithOne c l)
  where                                           -- Items for
ResidueLI
  module M = IdealPack c l upR1
  open M using (Subring; module Subring; LeftIdeal; module LeftIdeal;
                DReductionLIdeal; module DReductionLIdeal; ResidueLI;
                module ResidueLI; resI
               )
  R1 = UpRingWithOne.ringWithOne upR1
  open RingWithOne R1 using (_≈_; _-_)
       renaming (Carrier to C; isEquivalence to ≈equiv)


  residueSetoid : DReductionLIdeal → Setoid (setoidLevel c l) 0L
  residueSetoid   rdI =

           record{ Carrier = rCarr; _≈_ = _=r_; isEquivalence = isEq-r }
     where
     rCarr = ResidueLI rdI

     -- module Res-rdI = ResidueLI rdI                       
     -- open Res-rdI using (resRepr)     
     -- resRepr = ResidueLI.resRepr rCarr 
                   
     open ResidueLI using (resRepr)

     open DReductionLIdeal rdI using ()
                 renaming (leftIdeal to I; reductionByGens to reduction)
     open LeftIdeal I           using (extSubring)
     open Subring   extSubring  using (extSubDSet)
     open SubDSet   extSubDSet  using (member?; memberC?)

     congMem : {x y : C} → x ≈ y → memberC? x ≡ memberC? y
     congMem x=y =  Π.cong member? x=y

     _-rr_ : rCarr → rCarr → C
     _-rr_ =  _-_ on resRepr

     postulate _=r_   : Rel rCarr _
     postulate isEq-r : IsEquivalence _=r_

     g : rCarr -> C
     g = resRepr

     f : C -> C
     f x = resRepr (resI x)    -- (*)
----------------------------------------------------------------------



Thank you in advance for explanation,

------
Sergei