<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> </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 <dominique.devriese@cs.kuleuven.be><br> <b><span style="font-weight: bold;">To:</span></b> Serge D. Mechveliani <mechvel@botik.ru> <br><b><span style="font-weight: bold;">Cc:</span></b> Agda List <agda@lists.chalmers.se> <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> module test where<br><br> data ⊤ : Set where tt : ⊤<br><br> data P : ⊤ → Set where<br> pt : P tt<br><br> test : (t : ⊤) → P t<br> test t with t<br> test t | tt = {!result!}<br> 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. 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> test₂ : (t : ⊤) → P t<br> test₂ t = go t t<br>
where go : (t : ⊤) → (t' : ⊤) → P t<br> go t tt = result<br> 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 <<a ymailto="mailto:mechvel@botik.ru" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>>:<br>> On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:<br>>> Sorry, I cannot explain this, because I cannot run your example<br>>> (incomplete). --Andreas<br>>><br>><br>><br>> http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip<br>><br>> contains the precise Main.agda and readme.agda<br>>
(please, read first readme.agda).<br>> I am sorry: the proggram is large.<br>> I tried to present a small example, but have failed.<br>> Of course, it can be reduced, say, 10 times, but this would need a<br>> considerable effort.<br>> It looks like I am currently stuck in my attempt to write a library.<br>><br>> Thank you in advance for help,<br>><br>> -------<br>> Sergei<br>><br>><br>><br>>> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:<br>>> >Dear all,<br>>> >the attachement t.agda.zip<br>>> ><br>>> >contains a small code example where the same declaration of kind<br>>> > postulate p : <signature><br>>> >is taken in Agda-2.3.2 MAlonzo<br>>> >as a correct type for p or
not -- depending on whether p is set<br>>> >directly after ` = ' or in the last branch for `with'.<br>>> ><br>>> >Can you, please, explain this?<br>>> ><br>>> ><br>>> ><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>>> --<br>>> Andreas Abel <>< 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>>> http://www2.tcs.ifi.lmu.de/~abel/<br>>><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>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>