typefamily

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PatternSynonyms, TypeFamilies #-}

data K = A | B | C {-| Illegal-}

type family App (k :: K) (k' :: K) :: K where
  App 'B 'B = 'A
  App 'C 'C = 'B
  {-App _ _   = 'Illegal-}

data T (k :: K) where
  CT :: T 'A
  ET :: T k
  AT :: T k -> T k' -> T (App k k')

type A = T 'A
type B = T 'B
type C = T 'C

pattern TA :: B -> B -> A
pattern TA xb yb = AT xb yb

pattern TB :: C -> C -> B
pattern TB xc yc = AT xc yc