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