<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    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 class="moz-txt-link-freetext" 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 class="moz-txt-link-freetext" 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<br>
    <br>
    <div class="moz-cite-prefix">On 4/5/22 06:42, Jason Hu wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:MW4PR04MB7281912AF5ABE2E89CB5BD41AFE49@MW4PR04MB7281.namprd04.prod.outlook.com">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <meta name="Generator" content="Microsoft Word 15 (filtered
        medium)">
      <style>@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;}p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0in;
        font-size:11.0pt;
        font-family:"Calibri",sans-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;}.MsoChpDefault
        {mso-style-type:export-only;}div.WordSection1
        {page:WordSection1;}ol
        {margin-bottom:0in;}ul
        {margin-bottom:0in;}</style>
      <div class="WordSection1">
        <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"">a-function x y z</span><o:p></o:p></p>
        <p class="MsoNormal"><span style="font-family:"Courier
            New"">  with a-term-that-is-in-the-goal</span><o:p></o:p></p>
        <p class="MsoNormal"><span style="font-family:"Courier
            New"">...  | 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" type="1" start="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"">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>
      </div>
      <br>
      <fieldset class="moz-mime-attachment-header"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
  </body>
</html>