Idris - erasure of indices fails

I am currently trying to erase all unused indices from my Idris program - in one case however, the Idris compiler sees indices as reachable. I tried to replicate the behaviour in the following minimal example:

module Main

%access public export

-- CUSTOM VECTOR TYPES
data VectA : Nat -> Type -> Type where
    VNilA  : VectA Z a
    VConsA : a -> VectA len a -> VectA (S len) a

data VectB : Nat -> Type -> Type where
    VNilB  : VectB Z a
    VConsB : a -> VectB len a -> VectB (S len) a

-- THE FOLLOWING FUNCTIONS ARE USED TO CREATE A
-- CUSTOM VECTOR WHERE THE SIZE IS UNKNOWN
fromList : (l : List a) -> VectA (length l) a
fromList []      = VNilA
fromList (x::xs) = VConsA x (fromList xs)

createList : String -> List Int
createList "42" = [42, 42, 42]
createList _    = [1, 2, 3, 4]

-- SOME NESTED TRANSFORMATION FUNCTIONS ON VECT
transformVectA : VectA n a -> Maybe (VectB n a)
transformVectA VNilA         = Just VNilB
transformVectA (VConsA v vs) = 
    case transformVectA vs of
       Just vs' => Just $ VConsB v vs'
       Nothing  => Nothing

transformVectB : VectA m a -> VectB n a -> Maybe (VectB n a)
transformVectB VNilA ws = Just ws
transformVectB (VConsA v vs) ws = transformVectB vs ws 

transformVect : VectA n a -> VectA m a -> Maybe (VectB n a)
transformVect VNilA         VNilB = Nothing
transformVect VNilA         VNilA = Nothing
transformVect vs            VNilA = Nothing
transformVect (VConsA v vs) xs    = 
    case transformVectA (VConsA v vs) of
        Nothing  => Nothing
        Just vs' => transformVectB xs vs'

main : IO ()
main = do
    (testArg :: _) <- getArgs
    ls <- pure $ createList testArg
    va <- pure $ fromList ls
    vb <- pure $ transformVect va va

    putStrLn "OK"

When this is compiled by running:

idris Erasure.idr -o Erasure --warnreach

...the following warnings are shown:

Main.transformVect: inaccessible arguments reachable:
n (no more information available)
m (no more information available)

I also have trouble reading the dumpcases when compiling with the additional option:

--dumpcases cases.txt

Why do these warnings appear ? Is there any information available about how Idris is handling erasure besides the Chapter 'Erasure By Usage Analysis' in the Tutorial ?