<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <tt>Hi all,<br>
      <br>
      This is indeed the right move. An additional trick one can play is
      to<br>
      use an *inductive* 4-place </tt><tt><tt>relation `Θ ≡ q ** Γ₂ ++
        Γ₁` instead of a mere<br>
        equality proof. With this extra structure, you will be able to
        perform<br>
        induction directly on the proof rather than having to do case
        analysis<br>
        on `</tt></tt><tt><tt><tt>Θ` and `Γ₂` and use the proof of
          equality to dismiss the impossible<br>
          cases. This should make the whole experience more pleasant.<br>
          <br>
          Best,<br>
          gallais<br>
          <br>
          <br>
        </tt></tt></tt>
    <div class="moz-cite-prefix">On 01/10/2020 09:44, Neel Krishnaswami
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:12cc95ae-b65b-e89a-1f52-893533175a87@cl.cam.ac.uk">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <p>Dear Daniel.</p>
      <p>In general, intrinsically typed representations are definitely
        the way to go when your object language does not have a
        conversion relation. <br>
      </p>
      <p>If your language does have a conversion or judgemental equality
        relation, then intrinsic representations are enormously harder
        to work with. The basic issue is that the datatype representing
        typing will have proof trees corresponding to derivations of
        judgemental equality, and quotienting by the derivation of
        convertibility is giant PITA. (This is still active research,
        and I'm not actually up to date on where the state of the art
        here is -- probably Thorsten knows.) <br>
      </p>
      <p>In your particular case, however, it looks like you have a
        different problem. The _._ constructor in your screen shot has
        the type: <br>
      </p>
      <blockquote>
        <p><tt>_·_ : ∀{Δ} {Γ₁ Γ₂ : Context Δ} {A B q} <br>
                → Γ₁ ⊢ A -⟨ q ⟩→ B <br>
                → Γ₂ ⊢ A<br>
                → (q ** Γ₂ ++ Γ₁) ⊢ B <br>
          </tt></p>
      </blockquote>
      <p>Here, the return type of the function has an index which has
        function calls in it:</p>
      <blockquote>
        <p><tt>    ... → (<b>q ** Γ₂ ++ Γ₁</b>) ⊢ B <br>
          </tt></p>
      </blockquote>
      <p>The Agda type inference algorithm uses unification, and
        unification problems involving calls to arbitrary functions are,
        in general, hopeless. <b>Unification and pattern match coverage
          will generally only work reliably if the return type's indices
          contain expressions made only from variables and data
          constructors. </b><br>
      </p>
      <p>If memory serves, Conor McBride calls indices containing
        function calls "green slime", and warns people never to touch
        it. The way to keep from being contaminated by green slime is to
        use an explicit equality -- if you change your datatype
        declaration to the following:<br>
      </p>
      <blockquote>
        <p><tt>_·_ : ∀{Δ} {Γ₁ Γ₂ Θ : Context Δ} {A B q} <br>
                → Γ₁ ⊢ A -⟨ q ⟩→ B <br>
                → Γ₂ ⊢ A<br>
                → Θ ≡ q ** Γ₂ ++ Γ₁<br>
                → Θ ⊢ B <br>
          </tt></p>
      </blockquote>
      The case splitter will see the variable <tt>Θ </tt>and happily
      introduce a case for the <tt>_·_ </tt>constructor. But in the
      case branch, you will possess the equality <tt>Θ ≡ q ** Γ₂ ++ Γ₁</tt>
      which you can use to do any necessary reasoning yourself, thereby
      sparing the match coverage algorithm from having to do arbitrary
      mathematical reasoning. <br>
      <p>Best,<br>
        Neel<br>
      </p>
      <div class="moz-cite-prefix">On 01/10/2020 04:48, Daniel Lee
        wrote:<br>
      </div>
      <blockquote type="cite"
cite="mid:CAJ-vFh9yjO3VF7s0EGAqXvTiDXG2tLCwWtGhYKVHHeJTHyDBwg@mail.gmail.com">
        <pre class="moz-quote-pre" wrap="">Hi all,

I'm super new to Agda and the Agda community. Hopefully this is the right
place to ask something like this, but please call me out if it isn't.


I'm working on an Agda development for a QTT formalization. I'm trying to
use an intrinsically typed representation for terms, but run into
unification issues when trying to define substitution.

Substitution:
[image: Screen Shot 2020-09-30 at 8.34.38 PM.png]

Error message:
[image: Screen Shot 2020-09-30 at 8.34.50 PM.png]

Application def:
[image: Screen Shot 2020-09-30 at 8.35.05 PM.png]

I'm sort of at a loss for how to get around this. Is the issue because of
the functions in the return type?

More broadly, it seems like intrinsic typing is the Agda way of doing
things, and gives a lot for free. And it works really well in the STLC
example given in the PLFA textbook. But for a more complicated type system
like this, I'm starting to think it might be easier to use extrinsic
typing? I've also had to rely on the REWRITE pragma which I just learned
isn't allowed in --safe due to potential non-convergence.
Does someone maybe have experience with this and could speak to pros/cons
of using intrinsic vs extrinsic typing here?

Thanks,
Daniel

</pre>
        <br>
        <fieldset class="mimeAttachmentHeader"></fieldset>
        <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947887249&sdata=J5IxVSpywjzqZdwaL%2Fzl7TGE3V%2B5lhLJfBo11IoUvbY%3D&reserved=0" originalsrc="https://lists.chalmers.se/mailman/listinfo/agda" shash="wELiWXsvklA7fXNTOFE9V7edeaGMgfHDZ8kL/ES8zHbNEbqQ55F5YnDoLcfZ3a5mtiADUz0WVXePwG1gJqi0BuuxqExJXQ2B7u7jTQx2dRGSMb2THJLm/1nC5UOOqjNw1MiMtcDwrucG2mUZfaZ9FlzqFTG4YeQHd0ki9HbvkVs=" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
      </blockquote>
      <pre class="moz-signature" cols="72">-- 
Neel Krishnaswami
<a class="moz-txt-link-abbreviated" href="mailto:nk480@cl.cam.ac.uk" moz-do-not-send="true">nk480@cl.cam.ac.uk</a></pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></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://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947907230&amp;sdata=%2FZY4zKWoYjDwh0yDY%2BO0S76IWk9WC5caow98WgTuBxw%3D&amp;reserved=0">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7Cec25fc40f26f43e1903108d865e62ade%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637371386947907230&amp;sdata=%2FZY4zKWoYjDwh0yDY%2BO0S76IWk9WC5caow98WgTuBxw%3D&amp;reserved=0</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>