<div dir="ltr"><div dir="ltr">You shouldn't rebind the R again in the type signature of parse″, instead you can just use the same R from the main parse′ function:</div><div dir="ltr"><br><div><font color="#3333ff">  {-# NON_TERMINATING #-}<br>  parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>  parse′ {R} p₀ = parse″ p₀<br>    where<br>      parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R<br>      parse″ {xs = xs} p [] = Colist.fromList xs<br>      parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'<br>      ... | false = parse″ (∂ p t) (♭ s)<br>      ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))<br></font></div><br>-- Jesper</div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Sep 13, 2018 at 5:02 PM Serge Leblanc <<a href="mailto:33dbqnxpy7if@gmail.com">33dbqnxpy7if@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  

    
  
  <div text="#000000" bgcolor="#FFFFFF">
    Dear all, how do indicate that p₀ and p have the same type in this
    above example? Apparently, {R = R} is not enough.<br>
    Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en
    ĉi supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.<br>
    <p><font color="#3333ff">  {-# NON_TERMINATING #-}<br>
          parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>
          parse′ {R} p₀ = parse″ p₀<br>
            where<br>
              parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>
              parse″ {xs = xs} p [] = Colist.fromList xs<br>
              parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'<br>
              ... | false = parse″ (∂ p t) (♭ s)<br>
              ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))</font></p>
    <p>Sinceran dankon pro via venonta helpo.<br>
    </p>
    <p>-- <br>
    </p>
    <div class="m_-2097252034288942719moz-signature">Serge Leblanc
      <hr>
      gpg --search-keys 0x67B17A3F
      <br>
      Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>