<div dir="ltr"><div><div><div>lpaste here: <a href="http://lpaste.net/114815">http://lpaste.net/114815</a><br><br></div>I am aware that a function generated by &quot;with&quot; is not always well-typed. I&#39;m to understand this is limited to cases where, for example, function foo takes as its argument B (bar a), where a : A and B : A -&gt; Set, and we have rewritten &quot;bar a&quot; to some &quot;w&quot;, but foo remains untouched (i.e. its external to the context).<br><br></div>However, this is <b>not</b> that situation here. Agda has mysteriously eaten n : Nat, and replaced its occurrences with a : A (a parametric type), generating a type error. I can&#39;t imagine this is anything other than a bug, but if it isn&#39;t I&#39;d at least like to know the rationale behind this behaviour.<br><br></div>Note that I am aware that this definition of &quot;swap&quot; is terrible. I was playing with Agda to see if I could push it to see the function is involutive even in such a situation when I encountered this.<br><div><br>Thanks.<br clear="all"><div><div><div><div><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div></div></div></div></div></div>