haskell - 为什么这段代码不侵犯 "saturation requirement of type families"？

Question

我有这个将类型族映射到类型级列表的最小工作示例(从 singletons 库中挑选):

{-# 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    

它似乎工作:

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

代码在帖子 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 的评论中挑选出来的信息来回答我自己的问题。

原来我的代码确实违反了饱和度要求。由于 :kind! 的奇怪行为(错误？)，我没有找到错误。在 ghci 中。但是在 hs 文件本身中写入类型会产生编译错误。
TyCon1不适用于类型族，而是用于包装常规类型构造函数，如 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类型族不与任何类型变量统一。