<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>For what it's worth, the problematic code as quoted here type checks for me. That is to say, this statement:</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>"</span><span style="font-family: 'times new roman', 'new york', times, serif; font-size: 16px; ">Note that result is not accepted</span><span style="background-color: transparent; ">"</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0);
 font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>is false on my system.</span></div><div></div><div>&nbsp;</div><div>- darryl<br></div>  <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1">  <b><span style="font-weight:bold;">From:</span></b> Dominique Devriese &lt;dominique.devriese@cs.kuleuven.be&gt;<br> <b><span style="font-weight: bold;">To:</span></b> Serge D. Mechveliani &lt;mechvel@botik.ru&gt; <br><b><span style="font-weight: bold;">Cc:</span></b> Agda List &lt;agda@lists.chalmers.se&gt; <br> <b><span style="font-weight: bold;">Sent:</span></b> Tuesday, March 5, 2013 11:05 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] with match changes the result type of a function<br> </font>
 </div> <br>
Serge,<br><br>I've taken a brief look at your code, and I think this is a simplified<br>version of your problem:<br><br>&nbsp; module test where<br><br>&nbsp; data ⊤ : Set where tt : ⊤<br><br>&nbsp; data P : ⊤ → Set where<br>&nbsp; &nbsp; pt : P tt<br><br>&nbsp; test : (t : ⊤) → P t<br>&nbsp; test t with t<br>&nbsp; test t | tt = {!result!}<br>&nbsp; &nbsp; where postulate result : P t<br><br>Note that result is not accepted despite the fact that it has exactly<br>the declared type of test's result, which I believe is what you are<br>seeing in your code as well.&nbsp; The problem is that test's result type<br>is changed when you do a with-match on t, by substituting tt for t. A<br>solution is to replace your use of with by an explicit helper<br>function, where you can tightly control exactly which occurrences of<br>the with-scrutinee are replaced by the pattern:<br>&nbsp; test₂ : (t : ⊤) → P t<br>&nbsp; test₂ t = go t t<br>&nbsp;
 &nbsp; where go : (t : ⊤) → (t' : ⊤) → P t<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; go t tt = result<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; where postulate result : P t<br><br>By the way, in your case, the occurrence of the with-scrutinee in the<br>result type of your function is hidden by some calls, but Agda looks<br>through this and I believe the problem is the same as what I've<br>described above.<br><br>Regards<br>Dominique<br><br><br>2013/3/5 Serge D. Mechveliani &lt;<a ymailto="mailto:mechvel@botik.ru" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt;:<br>&gt; On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:<br>&gt;&gt; Sorry, I cannot explain this, because I cannot run your example<br>&gt;&gt; (incomplete). --Andreas<br>&gt;&gt;<br>&gt;<br>&gt;<br>&gt;&nbsp; &nbsp;  http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip<br>&gt;<br>&gt; contains the precise&nbsp; Main.agda&nbsp; and&nbsp; readme.agda<br>&gt;
 (please, read first&nbsp; readme.agda).<br>&gt; I am sorry: the proggram is large.<br>&gt; I tried to present a small example, but have failed.<br>&gt; Of course, it can be reduced, say, 10 times, but this would need a<br>&gt; considerable effort.<br>&gt; It looks like I am currently stuck in my attempt to write a library.<br>&gt;<br>&gt; Thank you in advance for help,<br>&gt;<br>&gt; -------<br>&gt; Sergei<br>&gt;<br>&gt;<br>&gt;<br>&gt;&gt; On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:<br>&gt;&gt; &gt;Dear all,<br>&gt;&gt; &gt;the attachement&nbsp; t.agda.zip<br>&gt;&gt; &gt;<br>&gt;&gt; &gt;contains a small code example where the same declaration of kind<br>&gt;&gt; &gt;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;  postulate p : &lt;signature&gt;<br>&gt;&gt; &gt;is taken in&nbsp;  Agda-2.3.2 MAlonzo<br>&gt;&gt; &gt;as a correct type for&nbsp; p&nbsp; or
 not&nbsp; -- depending on whether&nbsp; p&nbsp; is set<br>&gt;&gt; &gt;directly after ` = ' or in the last branch for `with'.<br>&gt;&gt; &gt;<br>&gt;&gt; &gt;Can you, please, explain this?<br>&gt;&gt; &gt;<br>&gt;&gt; &gt;<br>&gt;&gt; &gt;<br>&gt;&gt; &gt;_______________________________________________<br>&gt;&gt; &gt;Agda mailing list<br>&gt;&gt; &gt;<a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>&gt;&gt; &gt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>&gt;&gt; &gt;<br>&gt;&gt;<br>&gt;&gt; --<br>&gt;&gt; Andreas Abel&nbsp; &lt;&gt;&lt;&nbsp; &nbsp; &nbsp; Du bist der geliebte Mensch.<br>&gt;&gt;<br>&gt;&gt; Theoretical Computer Science, University of Munich<br>&gt;&gt; Oettingenstr. 67, D-80538 Munich, GERMANY<br>&gt;&gt;<br>&gt;&gt; <a ymailto="mailto:andreas.abel@ifi.lmu.de"
 href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>&gt;&gt; http://www2.tcs.ifi.lmu.de/~abel/<br>&gt;&gt;<br>&gt; _______________________________________________<br>&gt; Agda mailing list<br>&gt; <a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div>  </div></body></html>