Function only works when flipped

Question

Why does it error?

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

This only runs if I flip 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)

But it works with an explicit ls:

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

Answer 1

The errors comes from integerToFin : Integer -> (n : Nat) -> Maybe (Fin n). It is used by the REPL because you use (0 ** 0) instead of (FZ ** FZ). The REPL knows that this is just syntax and you really want a Fin n and not an Integer. So the REPL first tries to convert and (0 ** 0) becomes internally (integerToFin 0 n ** integerToFin 0 m). Because of the type inference implementation it thinks about the case of n=Z. And so integerToFin 0 Z = Nothing instead of Just Fin n.

To solve this you could help a bit:

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

Or

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

---

So, why does this error?

This depends on the implementation of the type inference of the compiler and if I see this correct, it is just not smart enough for this case. :-)

I guess the problem is roughly the following:

This is :t nproject:

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

n could be 0 and thus integerToFin 0 0 = Nothing.

In the flipped case, n is known to be 1, because it tries to infer the implicit arguments and [[0]] before (0 ** 0). Then the REPL can infer that integerToFin 0 (S Z) = Just FZ