{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
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
    -- | b ab -> a
  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