data TyFun

type family App f a :: l

data TC

type f $ x