なぜこのコードは「型ファミリの飽和要件」に違反しないのですか？

Question

私はタイプレベルのリスト上のタイプの家族をマッピングする（singletonsライブラリから抜粋）この最小限の作業例を持っています。

ghci> :set -XDataKinds 
ghci> :kind! Map (TyCon1 Flip) '[Char,Int] 
Map (TyCon1 Flip) '[Char,Int] :: [*] 
= '[Int, Char] 

コードを説明します

{-# language PolyKinds #-} 
{-# language DataKinds #-} 
{-# language TypeFamilies #-} 
{-# language TypeOperators #-} 

data TyFun :: * -> * -> * 

data TyCon1 :: (k1 -> k2) -> (TyFun k1 k2 -> *) 

type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2 
type instance Apply (TyCon1 f) x = f x 

type family Map (f :: TyFun a b -> *) (as :: [a]) :: [b] where 
    Map f '[] = '[] 
    Map f (x ': xs) = Apply f x ': Map f xs 

type family Flip t :: * where 
    Flip Int = Char 
    Flip Char = Int  

動作するようです投稿の中でDefunctionalization for the win。これは、 "GHCは型変数を型族と統一させません"という事実を回避する方法です。これは「タイプファミリの飽和要件」と呼ばれます。

私の疑いがある：私たち「実行」:kind! Map (TyCon1 Flip) '[Char,Int]ラインtype instance Apply (TyCon1 f) x = f xで、fは、私たちのFlip型家族と照合されます、と思われるとき。なぜこれは飽和要件を侵害しないのですか？

Answer 1

私は自分の質問にdfeuerとuser2407038のコメントから情報を得て答えています。

私のコードはが飽和要件を侵していたことが判明しました。 ghciの:kind!という奇妙な動作（バグ？）のために私はエラーを見つけられませんでした。しかし、ファイルをhsファイルに書き込むと、コンパイルエラーが発生します。

は、タイプファミリではなく、タイプ変数との統合に問題がないMaybeのような通常型コンストラクタをラップします。たとえば、type Foo = Map (TyCon1 Maybe) '[Char,Int]はうまく動作します。

タイプファミリでは、それぞれに特殊な補助タイプを定義し、そのタイプのApplyインスタンスを定義する必要があります。このように：

data FlipSym :: TyFun * * -> * 
type instance Apply FlipSym x = Flip x 

type Boo = Map FlipSym '[Char,Int] 

お知らせそのFlipタイプの家族はどのようなタイプの変数に統一されていないこの方法。