haskell - 暗黙の引数と型ファミリー

Question

私は Data.Singletons ライブラリを使用して、依存型付けされたプログラムを実験してきました。これは、論文「シングルトンを使用した依存型付けプログラミング」で長さの注釈が付けられたベクトルの開発に続き、次の問題に遭遇しました。

次のコードは、 function の定義を除いて、indexIGHC 7.6.3 で型チェックを行い、それがなくても期待どおりに動作します。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons
import Data.Singletons.TH

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Eq

$(genSingletons [''Nat])

data FlipList :: * -> * -> Nat -> * where
    Cons :: ((a -> b) -> a -> b) -> FlipList a (a -> b) n -> FlipList a b (S n)
    Nil :: FlipList a b Z

type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Z = 'False
type instance Z :< (S n) = 'True
type instance (S m) :< (S n) = m :< n

type family PreMap a b (m :: Nat) :: *
type instance PreMap a b Z = a -> b
type instance PreMap a b (S n) = PreMap a (a -> b) n

type family BiPreMap a b (m :: Nat) :: *
type instance BiPreMap a b m = PreMap a b m -> PreMap a b m

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = f
index (SS sm) (Cons _ fl) = index sm fl

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

を含めた後indexI、GHC は 2 つのエラーを生成します。

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

と、

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

いずれの誤りの根源も、項withSing indexが 型FlipList a b n -> BiPreMap a b a0を持ち、 を推論できなければa0 ~ m、GHC が を証明できないことにあるようBiPreMap a b m ~ BiPreMap a b a0です。型ファミリの型推論には、ADTS を使用するときに得られる便利さ (単射性、生成性など) のほとんどが欠けていることはわかっていますが、この場合の問題が正確に何であるか、およびそれを回避する方法についての私の理解は非常に限られています。 . それを解決する可能性のある指定できる制約はありますか?