<div dir="ltr">If anyone wants to typecheck the code, it is in the 54th commit of <a href="https://github.com/xekoukou/sparrow" target="_blank">https://github.com/xekoukou/<wbr>sparrow</a> , in the agda folder.<br><div><br><br>This is the piece of code that I am trying to change and that creates the error:<br><br>"<br>     <span class="gmail-m_-5564469921218119262gmail-pl-en">_⊂_</span> <span class="gmail-m_-5564469921218119262gmail-pl-k">:</span> {i : Size} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {j : Size< ↑ i} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {k : Size< ↑ j} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> <span class="gmail-m_-5564469921218119262gmail-pl-k">∀</span>{pll ll ell rll} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {ind : IndexLL {i} pll ll} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> (elf : LFun {_} {i} {j} {ell} {pll})
      
      
        <table class="gmail-m_-5564469921218119262gmail-highlight gmail-m_-5564469921218119262gmail-tab-size gmail-m_-5564469921218119262gmail-js-file-line-container"><tbody><tr><td id="gmail-m_-5564469921218119262gmail-LC33" class="gmail-m_-5564469921218119262gmail-blob-code gmail-m_-5564469921218119262gmail-blob-code-inner gmail-m_-5564469921218119262gmail-js-file-line">           <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {{prf : usesInput elf}} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> LFun {_} {j} {k} {rll} {(replLL ll ind ell)}</td>
      </tr>
      <tr>
        </tr></tbody></table>           <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> LFun {_} {i} {k} {rll} {ll}<br>"<br><br></div><div>Removing "i" from "elf" results into error into a piece of code that uses the constructor.<br><br></div><div>"<br>     <span class="gmail-m_-5564469921218119262gmail-pl-en">_⊂_</span> <span class="gmail-m_-5564469921218119262gmail-pl-k">:</span> {i : Size} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {j : Size< ↑ i} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {k : Size< ↑ j} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> <span class="gmail-m_-5564469921218119262gmail-pl-k">∀</span>{pll ll ell rll} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {ind : IndexLL {i} pll ll} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> (elf : LFun {_} {_} {j} {ell} {pll})
      
      
        <table class="gmail-m_-5564469921218119262gmail-highlight gmail-m_-5564469921218119262gmail-tab-size gmail-m_-5564469921218119262gmail-js-file-line-container"><tbody><tr><td id="gmail-m_-5564469921218119262gmail-LC33" class="gmail-m_-5564469921218119262gmail-blob-code gmail-m_-5564469921218119262gmail-blob-code-inner gmail-m_-5564469921218119262gmail-js-file-line">           <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> {{prf : usesInput elf}} <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> LFun {_} {j} {k} {rll} {(replLL ll ind ell)}</td>
      </tr>
      <tr>
        </tr></tbody></table>           <span class="gmail-m_-5564469921218119262gmail-pl-k">→</span> LFun {_} {i} {k} {rll} {ll}<br>"<br><br></div><div>It seems to me though that the size of pll is deducible from "ind". ind is annotated to have size i which means that both "pll" and "ll" have size "i".<br><br></div><div>The error that I see is that it considers the size of "pll" to be "j" and not "i".<br></div><div><br><br></div></div>