Why doesn't this code infringe the "saturation requirement of type families"?

Question

I have this minimal working example (culled from the singletons library) of mapping a type family over a type-level list:

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

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 post Defunctionalization for the win. It is a workaround for the fact that "GHC will not let a type variable unify with a type family". This is called the "saturation requirement of type families".

My doubt is: when we "run" :kind! Map (TyCon1 Flip) '[Char,Int] it seems that , in the line type instance Apply (TyCon1 f) x = f x, f will be matched with our Flip type family. Why doesn't this infringe the saturation requirement?

Answer 1

I'm answering my own question with information culled from dfeuer and user2407038's comments.

Turns out that my code did infringe the saturation requirement. I didn't find the error because of a strange behaviour (bug?) of :kind! in ghci. But writing the type in the hs file itself gives a compilation error.

TyCon1 is not for type families, but for wrapping regular type constructors like Maybe, that have no problem unifying with type variables. type Foo = Map (TyCon1 Maybe) '[Char,Int] works fine, for example.

For type families, we need to define a special auxiliary 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]

Notice that this way the Flip type family is not unifying with any type variable.