Unificación algoritmo infiere demasiado tipos de hormigones

Question

Yo estaba tratando de crear Tuplas de tamaño n en Idris:

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)

Pero estoy recibiendo este error en la última línea:

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

Hay una manera de hacer que esta función trabaje?

Answer 1

El problema es que insertAt (FS i) a types no puede ser reducido sin saber nada acerca de types.Si lo sabía types = t :: ts a continuación, se puede reducir a t :: insertAt i ts.

Pero en el segundo caso de mapN, nos ¿ saber que types es exactamente de que forma:

1. Nuestro primer argumento es FS i
2. Lo que implica n = S m para algunos m...
3. Lo que significa que nuestro implícito types el argumento tiene el tipo Vect (S m) Type
4. Lo que significa que es de la forma t :: ts!

Una vez que este a Idris, es feliz para reducir insertAt (FS i) a types y así, su código typechecks:

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