vector - Idris - 索引擦除失败

Question

我目前正试图从我的 Idris 程序中删除所有未使用的索引 - 然而，在一种情况下，Idris 编译器认为索引是可访问的。我尝试在以下最小示例中复制该行为：

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"

当通过运行编译时：

idris Erasure.idr -o Erasure --warnreach

...显示以下警告：

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

使用附加选项编译时，我也无法阅读转储箱：

--dumpcases case.txt

为什么会出现这些警告？除了教程中的“按使用分析擦除”一章之外，是否有任何关于 Idris 如何处理擦除的信息？

标签： vectoridrisdependent-type