Implementing Total Parsers in Idris Based on a Paper on Agda

Question

I am trying to implement total parsers with Idris, based on this paper. First I tried to implement the more basic recogniser type P:

Tok : Type
Tok = Char

mutual
  data P : Bool -> Type where
    fail : P False
    empty : P True
    sat : (Tok -> Bool) -> P False
    (<|>) : P n -> P m -> P (n || m)
    (.) : LazyP m n -> LazyP n m -> P (n && m)
    nonempty : P n -> P False
    cast : (n = m) -> P n -> P m

  LazyP : Bool -> Bool -> Type
  LazyP False n = Lazy (P n)
  LazyP True  n = P n

DelayP : P n -> LazyP b n
DelayP {b = False} x = Delay x
DelayP {b = True } x = x

ForceP : LazyP b n -> P n
ForceP {b = False} x = Force x
ForceP {b = True } x = x

Forced : LazyP b n -> Bool 
Forced {b = b} _ = b

This works fine, but I cannot work out how to define the first example from the paper. In Agda it is:

left-right : P false
left-right = ♯ left-right . ♯ left-right

But I cannot get this to work in Idris:

lr : P False
lr = (Delay lr . Delay lr)

produces

Can't unify 
    Lazy' t (P False)
with
    LazyP n m

It will typecheck if you give it some help, like this:

lr : P False
lr = (the (LazyP False False) (Delay lr)) . (the (LazyP False False) (Delay lr))

But this is rejected by the totality checker, as are other variants like

lr : P False
lr = Delay (the (LazyP True False) lr) . (the (LazyP False False) (Delay lr))

It doesn't help that I'm not entirely sure how the ♯ operator binds in Agda.

Can anyone see a way to get define the left-right recogniser in Idris? Is my definition of P wrong, or my attempt at translating the function? Or is Idris's totality checker just not quite up to this coinductive stuff?

Avoirdupois

Answer 1

Currently trying to port this library myself, it seems like Agda infers different implicits to Idris. These are the missing implicits:

%default total

mutual
  data P : Bool -> Type where
    Fail : P False
    Empty : P True
    Tok : Char -> P False
    (<|>) : P n -> P m -> P (n || m)
    (.) : {n,m: Bool} -> LazyP m n -> LazyP n m -> P (n && m)

  LazyP : Bool -> Bool -> Type
  LazyP False n = Inf (P n)
  LazyP True  n = P n

lr : P False
lr = (.) {n=False} {m=False} (Delay lr) (Delay lr)

Ayeaye

This works! I've been away from this for so long it will take me a bit of time to properly re-grok this and work out why it works. I'll accept once I can do that. – Avoirdupois