sdfsd.idr

data LQueue : Nat -> Type -> Type where
  MkQ : (xs : Vect ln a)
     -> (ys : Vect rn a)
     -> LQueue (ln + rn) a

-- an invariant checker
queue : LQueue n a -> LQueue n a
queue (MkQ xs {ln} ys {rn}) with (isLTE rn ln)
  queue (MkQ xs ys) | (Yes prf) = MkQ xs ys
  queue (MkQ xs {ln} ys {rn}) | (No contra) = 
    rewrite sym $ plusZeroRightNeutral (ln + rn)
    in MkQ (xs ++ reverse ys) []

snoc : LQueue n a -> a -> LQueue (S n) a
snoc (MkQ xs {ln} ys {rn}) y =
    rewrite plusSuccRightSucc ln rn
    in queue $ MkQ xs (y :: ys)

-- **** my issue ****
-- idris can't reconcile that (y :: ys) accounts for (S n)
-- probably due to the typical 'left biased plus' problem
-- Is there any possible way to use/allow rewrite for the pattern match?
-- Or can I construct a lemma elswhere somehow?
-- I don't know how to approach this since it's in the pattern world
tail : LQueue (S n) a -> LQueue n a
tail (MkQ (x :: xs) ys) = queue (MkQ xs ys)
tail (MkQ xs (y :: ys)) = ?pattern_match_failure

{- errormsg
When checking left hand side of Data.PF.Queue.LQ.tail:
When checking an application of Data.PF.Queue.LQ.tail:
        Type mismatch between
                LQueue (ln + S len) a (Type of MkQ xs (y :: ys))
        and
                LQueue (S n) a (Expected type)
        
        Specifically:
                Type mismatch between
                        plus ln (S len)
                and
                        S n
-}