[Agda] record field ambiguity

Sergei Meshveliani mechvel at botik.ru
Thu May 9 13:07:45 CEST 2013

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 


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

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

       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)
  record DReductionLIdeal : Set (setoidLevel c l)
    field  upLeftIdeal : UpLeftIdeal

  record ResidueLI (I : DReductionLIdeal) : Set (setoidLevel c l)
    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
  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 }
     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,


More information about the Agda mailing list