統一アルゴリズム透視型の種類

Question

IDRISのサイズ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の2番目の場合では、typesがその形式であることを知っています。

1. 私たちの最初の引数はFS i
です。
2. n = S mのためのmを意味する...
3. 意味私たちの暗黙のtypes引数にはVect (S m) Type
があります。
4. これはそれがt :: tsの形式であることを意味します！

これをiDRISに指摘したら、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

.