Idris - Vector Queues and Rewrite Rules

Question

I'm trying to implement something like a functional queue in Idris, but which carries the number of elements in the type - such as Queue ty n m (n+m) where n is the number of elements in one Vect n ty, m is the elements in a second Vect m ty, and (n+m) is the total elements.

The problem is, I'm running into problems with applying rewrite rules when manipulating these sizes as implicit arguments:

module Queue

import Data.Vect as V

data Queue : Type -> Nat -> Nat -> Nat -> Type where
    mkQueue : (front : V.Vect n ty)
           -> (back : V.Vect m ty)
           -> Queue ty n m (n + m)

%name Queue queue

top : Queue ty n m (S k) -> ty
top {n = S j} {m} {k = j + m} (mkQueue front back) =
    V.head front
top {n = Z} {m = S j} {k = j} (mkQueue front back) =
    V.head $ V.reverse back

bottom : Queue ty n m (S k) -> ty
bottom {m = S j} {n} {k = n + j} (mkQueue front back) = 
    ?some_rewrite_1 (V.head back)
bottom {m = Z} {n = S j} {k = j} (mkQueue front back) = 
    ?some_rewrite_2 (V.head $ V.reverse front)

top works but bottom does not. It would appear that I somehow need to supply plusZeroRightNeutral and plusRightSuccRight rewrites, but I'm not sure where to put those, or whether there might be another option. Here are the error messages:

Error on first line of bottom:

         Type mismatch between
                 Queue ty n (S j) (n + S j) (Type of mkQueue front back)
         and
                 Queue ty n (S j) (S (n + j)) (Expected type)

         Specifically:
                 Type mismatch between
                         plus n (S j)
                 and
                         S (n + j)

Error on second line of bottom:

         Type mismatch between
                 Queue ty (S j) 0 (S j + 0) (Type of mkQueue front back)
         and
                 Queue ty (S j) 0 (S j) (Expected type)

         Specifically:
                 Type mismatch between
                         plus (S j) 0
                 and
                         S j

The individual sizes tell me when I need to rotate the two Vects, and the overall size tells me when I have an empty vs. non-empty Queue, so I do want to track all the information if possible.

Answer 1

One possible way of solving this problem is to destruct n as well. This time Idris understands that the last argument is not zero, which it is basically complaining about:

total
bottom : Queue ty n m (S k) -> ty
bottom {m = S m} {n = S n} (MkQueue _ back) = V.head back
bottom {m = S m} {n = Z}   (MkQueue _ back) = V.head back
bottom {m = Z}   {n = S n} (MkQueue front _) = V.head $ V.reverse front
bottom {m = Z}   {n = Z}   (MkQueue _ _) impossible

As a side note, I'd suggest to make the top function total:

total
top : Queue ty n m (S k) -> ty
top {n = S n}           (MkQueue front _) = V.head front
top {n = Z}   {m = S m} (MkQueue _ back) = V.head $ V.reverse back
top {n = Z}   {m = Z}   (MkQueue _ _) impossible