功能仅在翻转时起作用

Question

为什么会出错？

import Data.Vect
import Data.Vect.Quantifiers
get : (i : Fin n) -> All (flip Vect t) ls -> Vect (index i ls) t
get FZ (y :: z) = y
get (FS y) (z :: w) = get y w
nproject : Vect l (n : _  ** Fin (index n ls)) -> All (flip Vect t) ls -> Vect l t
nproject [] _ = []
nproject ((n ** i)::fs) vs = index i (get n vs) :: nproject fs vs

这仅在我翻转nproject时运行：

*VectExtensions> flip nproject [[0]] [(0 ** 0)]
[0] : Vect 1 Integer
*VectExtensions> nproject [(0 ** 0)] [[0]]
When checking argument pf to constructor Builtins.MkDPair:
        Type mismatch between
                IsJust (Just x)
        and
                IsJust (integerToFin 0 n)

，但可与显式ls：

一起使用

*VectExtensions> nproject {ls=[_]} [(0 ** 0)] [[0]]
[0] : Vect 1 Integer

Answer 1

错误来自 integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)。它是由repl使用的，因为您使用(0 ** 0)而不是(FZ ** FZ)。REPL知道这只是语法，您确实需要Fin n而不是Integer。因此，首先尝试转换，并且(0 ** 0)变为内部(integerToFin 0 n ** integerToFin 0 m)。由于类型的推理实现，因此考虑了n=Z的情况。因此，integerToFin 0 Z = Nothing代替Just Fin n。

要解决这个问题，您可以帮助一些：

> nproject [(FZ ** 0)] [[0]] 
[0] : Vect 1 Integer

或

> nproject [(0 ** FZ)] [[0]] 
[0] : Vect 1 Integer

---

那么，为什么这个错误？

这取决于编译器的类型推理的实现，如果我认为这是正确的，那么对于这种情况来说，它不够聪明。:-)

我猜这个问题大约是以下内容：

这是:t nproject：

nproject : Vect l (n : Fin n ** Fin (index n ls)) -> All (flip Vect t) ls -> Vect l t

n可以是0，因此可以integerToFin 0 0 = Nothing。

在翻转的情况下，n是1，因为它试图在(0 ** 0)之前推断隐式参数和[[0]]。然后可以推断 integerToFin 0 (S Z) = Just FZ