[Agda] A quiz: what should the types of these definitions be?

[Andreas Abel]

Hi, this is a poll about what you would expect Agda to do about the 
hiding of parameters if you have definitions inside a parametrized 
record inside a parametrized module.

(If you want to cheat, please be aware that different versions of Agda 
might give different answers. ;-))

module _ where

-- M1/R1: visible parameter
-- M2/R2: hidden parameter

module M1 (A : Set) where

   record R1 (B : Set) : Set where
     field f : A
     g = f
     id : B → B
     id x = x

   record R2 {B : Set} : Set where
     field f : A
     g = f
     id : B → B
     id x = x

module M2 {A : Set} where

   record R1 (B : Set) : Set where
     field f : A
     g = f
     id : B → B
     id x = x

   record R2 {B : Set} : Set where
     field f : A
     g = f
     id : B → B
     id x = x

m1r1f  : ?
m1r1f  = M1.R1.f

m1r1g  : ?
m1r1g  = M1.R1.g

m1r1id : ?
m1r1id = M1.R1.id

m1r2f  : ?
m1r2f  = M1.R2.f

m1r2g  : ?
m1r2g  = M1.R2.g

m1r2id : ?
m1r2id = M1.R2.id

m2r1f  : ?
m2r1f  = M2.R1.f

m2r1g  : ?
m2r1g  = M2.R1.g

m2r1id : ?
m2r1id = M2.R1.id

m2r2f  : ?
m2r2f  = M2.R2.f

m2r2g  : ?
m2r2g  = M2.R2.g

m2r2id : ?
m2r2id = M2.R2.id

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