Алгоритм унификации выводит слишком конкретные типы

Question

Я пытался создать кортежи размера n в Идрисе:

module NTuple

data Tuple : Vect n Type -> Type where
  EmptyTuple : Tuple Nil
  TupleItem : a -> Tuple types -> Tuple (a :: types)


mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN fZ     f (TupleItem x xs) = TupleItem (f x) xs
mapN (fS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)

Но я получаю эту ошибку в последней строке:

When elaborating left hand side of mapN: 
When elaborating an application of NTuple.mapN:
    Can't unify
            Tuple (a :: types)
    with
            Tuple (insertAt (fS i) a types)

    Specifically:
            Can't unify
                    a :: types
            with
                    insertAt (fS i) a types

Есть ли способ заставить эту функцию работать?

Answer 1

Проблема в том, что insertAt (FS i) a types не может быть уменьшено, ничего не зная о types.Если бы мы знали types = t :: ts тогда его можно было бы сократить до t :: insertAt i ts.

Но во втором случае mapN, мы делать знай это types имеет именно такую ​​форму:

1. Наш первый аргумент FS i
2. подразумевая n = S m для некоторых m...
3. Значение нашего неявного types аргумент имеет тип Vect (S m) Type
4. Это означает, что оно имеет вид t :: ts!

Как только мы укажем на это Идрису, он будет рад уменьшить insertAt (FS i) a types и, таким образом, ваш код проверяет тип:

mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN                  FZ     f (TupleItem x xs) = TupleItem (f x) xs
mapN {types = _ :: _} (FS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
mapN {types = []}     (FS i) _ _                = absurd i