{-# Language TypeFamilies, TypeInType , TypeOperators , UndecidableInstances #-}

module Compose where

import Data.Kind

data TyFun :: * -> * -> *

type a ~> b = TyFun a b -> *
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

type a @@ b = Apply a b
infixl 9 @@

data TyCon2 (tc :: a -> b -> c) (tf :: TyFun a (b ~> c))
data TyCon1 (tc :: a -> b) (tf :: TyFun a b)

type instance Apply (TyCon1 tc) a = tc a
type instance Apply (TyCon2 tc) a = TyCon1 (tc a)

--

data (:.$) :: (b ~> c) ~> (a ~> b) ~> (a ~> c)
type instance Apply (:.$) a = (:.$$) a

data (:.$$) :: (b ~> c) -> (a ~> b) ~> (a ~> c)
type instance Apply ((:.$$) a) b = (:.$$$) a b

data (:.$$$) :: (b ~> c) -> (a ~> b) -> (a ~> c)
type instance Apply ((:.$$$) a b) x = (:.$$$$) a b x

type (:.$$$$) a b x = (:.) a b x

type family (:.) (f :: b ~> c) (g :: a ~> b) (x :: a) :: c where
 (:.) f g x = f @@ (g @@ x)