Why does this code not violate the "requirement of saturation of type families"?

Question

I have this minimal working example (from the singletons library) for matching a type family in a list of type types:

{-# 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 = fx type family Map (f :: TyFun ab -> *) (as :: [a]) :: [b] where Map f '[] = '[] Map f (x ': xs) = Apply fx ': Map f xs type family Flip t :: * where Flip Int = Char Flip Char = Int 

It seems to work:

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

The code is explained in the message Functionalization to win . A workaround is the fact that "the GHC does not allow the union of a type type with a type family." This is called a "type family saturation requirement."

I doubt: when we "start" :kind! Map (TyCon1 Flip) '[Char,Int] :kind! Map (TyCon1 Flip) '[Char,Int] , it seems that in the line type instance Apply (TyCon1 f) x = fx , f will be mapped to our Flip type family. Why doesn't this violate saturation requirements?

Answer 1

I am answering my question with information received from dfeuer and user2407038 comments.

It turns out my code violated the saturation requirement. I did not find an error due to strange behavior (error?) :kind! in ghci. But writing the type in the hs file alone leads to a compilation error.

TyCon1 does not belong to type families, but for flowing around regular type constructors, such as Maybe , which have no problems with unifying type variables. type Foo = Map (TyCon1 Maybe) '[Char,Int] works fine, for example.

For type families, we need to define a special helper type for each of them, and then define an Apply instance for the type. Like this:

 data FlipSym :: TyFun * * -> * type instance Apply FlipSym x = Flip x type Boo = Map FlipSym '[Char,Int] 

Note that in this way, the Flip type family is not combined with any type variable.