<div dir="ltr">Hi all,<div><br></div><div>making extensive use of parametrized modules and records, I&#39;m wondering what&#39;s the proper mental model to predict how the normal forms of applied field selectors will show up, or maybe a summary of how this feature is implemented and where to look for it in the source.</div>
<div><br></div><div>My question is general, but I&#39;ll also add an example for concreteness:</div><div><br></div><div><div>    module Use where</div><div><br></div><div>    postulate</div><div>       A : Set</div><div>       I : Set</div>
<div><br></div><div>    module R (_ : I)  where</div><div>      postulate</div><div>        f : A</div><div><br></div><div>    postulate</div><div>      r : I</div><div>      X : I -&gt; I</div><div>      Q : A -&gt; Set</div>
<div><br></div><div>    module Qualified where</div><div>      K = X r</div><div>      open R K</div><div>  </div><div>      foo : Q f</div><div>      foo = { }0 -- normal form: Q (R.f (X r))                                                                                                             </div>
<div>    module UnQualified where<br></div><div>  </div><div>      open R (X r)</div><div><br></div><div>      foo : Q f</div><div>      foo = { }1 -- normal form: Q f                                                                                                                       </div>
<div><br></div><div>It&#39;s fairly counterintuitive that going through a simple definition like K alters the result, is it because we&#39;ve gone through a reduction expanding K during normalization? But, as I said, I&#39;ve little intuition over the whole issue.</div>
</div><div><br></div><div>By the way, I&#39;ve used the terms &quot;qualified&quot; and &quot;unqualified&quot; but the concern is really about not showing the parameters which I&#39;ve opened the module with.</div><div><br>
</div><div>My use cases tend to also include some rerouting of parameters that might make the reconstruction of the unqualified form harder:</div><div><br></div><div>  module X {A} {B} = Product (products A B)</div><div>  open X</div>
<div><br></div><div>at this point we usually get normal forms like `Product.someField (products A B) ...` rather than `someField ...` which is especially unreadable for mixfix operators because of how the value of the record takes the place of the first underscore in the name.</div>
<div><br></div><div><br></div><div>Thanks,</div><div>  Andrea</div></div>