[Agda] Type mismatch? Tipo miskongruas?

[Jesper Cockx]

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:

  {-# NON_TERMINATING #-}
  parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
  parse′ {R} p₀ = parse″ p₀
    where
      parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R
      parse″ {xs = xs} p [] = Colist.fromList xs
      parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'
      ... | false = parse″ (∂ p t) (♭ s)
      ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))

-- Jesper

On Thu, Sep 13, 2018 at 5:02 PM Serge Leblanc <33dbqnxpy7if at gmail.com>
wrote:

> Dear all, how do indicate that p₀ and p have the same type in this above
> example? Apparently, {R = R} is not enough.
> Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi
> supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.
>
>   {-# NON_TERMINATING #-}
>   parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
>   parse′ {R} p₀ = parse″ p₀
>     where
>       parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
>       parse″ {xs = xs} p [] = Colist.fromList xs
>       parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
>       ... | false = parse″ (∂ p t) (♭ s)
>       ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
>
> Sinceran dankon pro via venonta helpo.
>
> --
> Serge Leblanc
> ------------------------------
> gpg --search-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180913/8b58dcdb/attachment.html>