{-#
LANGUAGE
  DataKinds, PolyKinds, TypeFamilies, TypeOperators, MultiParamTypeClasses,
  FunctionalDependencies, FlexibleInstances, StandaloneKindSignatures,
  UndecidableInstances
#-}

module M where

import Data.Kind (Constraint)

type HasAppend :: [k] -> [k] -> [k] -> Constraint
class Append a b ~ ab => HasAppend a b ab | a ab -> b where
  type Append a b :: [k]
  
instance HasAppend '[] b b where
  type Append '[] b = b
  
instance HasAppend a b ab => HasAppend (x : a) b (x ': ab) where
  type Append (x : a) b = x ': Append a b