<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0in;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New",serif;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0in;
margin-right:0in;
margin-bottom:0in;
margin-left:.5in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:"Courier New",serif;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:2051953955;
mso-list-template-ids:-1;}
@list l0:level1
{mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level2
{mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level3
{mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level4
{mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level5
{mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level6
{mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level7
{mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level8
{mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level9
{mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Inspect idiom won’t work if with-abstraction itself does nothing.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I realize that it has something to do with the order of unification of definitions in where clauses. I suspect that when with-abstraction is abstracting over a term that depends on another term which contains unresolved metavariables (which
is resolvable but not yet at this moment), then with-abstraction is not going to do anything. Does that ring a bell for the dev team? Do you observe any similar problem coming from the order of unification? I think I have a clue on how to construct a smaller
reproduction. I will do so when I have time.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:godzbanebane@gmail.com">Georgi Lyubenov</a><br>
<b>Sent: </b>Tuesday, April 5, 2022 4:58 AM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
<b>Subject: </b>Re: [Agda] when with-abstraction fails?</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi!<br>
<br>
I can't give you a concrete reason or way to fix it, but when this happens for me, usually the "inspect idiom" fixes it. This is in the standard library, but as of recent, it's also been built into the language in some shape or form.<br>
<br>
See the section on the changelog on "inspect idiom" - <a href="https://github.com/agda/agda/blob/master/doc/release-notes/2.6.2.md">
https://github.com/agda/agda/blob/master/doc/release-notes/2.6.2.md</a><br>
and the documentation here - <a href="https://agda.readthedocs.io/en/v2.6.2.1/language/with-abstraction.html#with-abstraction-equality">
https://agda.readthedocs.io/en/v2.6.2.1/language/with-abstraction.html#with-abstraction-equality</a><br>
<br>
Cheers,<br>
Georgi<o:p></o:p></p>
<div>
<p class="MsoNormal">On 4/5/22 06:42, Jason Hu wrote:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal">Hi all,<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">I realize that in some situations, with-abstraction does nothing. E.g.<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New",serif">a-function x y z</span><o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New",serif"> with a-term-that-is-in-the-goal</span><o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New",serif">... | x = ?</span><o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">The with-abstraction does not report any error, but rather it does nothing. I know that in some situation with-abstraction is impossible but in those cases, Agda would throw an error. However, in other cases, a tiny bit of change in the
code would just turn with-abstraction into a noop and I don’t know why. <o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">I do encounter situations like this in my real project but I do not know how to concentrate a minimal reproducible example. However, I do realize the following methods might or might not solve this problem:<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<ol style="margin-top:0in" start="1" type="1">
<li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">Add more arguments to the function to a point where everything involved in
<span style="font-family:"Courier New",serif">a-term-that-is-in-the-goal</span> appears in the argument list.<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">If the previous method still doesn’t work (as it happens at this moment), then it seems to have something to do with deeply nested where clauses, e.g. if the example function above
is in a where clause, then moving it outside of the where clause will almost certainly make the with-abstraction work again.<o:p></o:p></li></ol>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">As a consequence of this problem, rewrite will also cease to work. Should I consider this a bug (which I really intend to) or is there some behavior that I don’t understand in Agda?<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"> <o:p></o:p></p>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<pre>_______________________________________________</pre>
<pre>Agda mailing list</pre>
<pre><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></pre>
</blockquote>
<pre style="mso-margin-top-alt:0in;margin-right:.5in;margin-bottom:5.0pt;margin-left:.5in"><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></pre>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Courier New",serif"><o:p> </o:p></span></p>
</div>
</body>
</html>