{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module M where

import Data.Kind
import Data.Proxy

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

bar :: Proxy (list :: [Type]) -> Proxy list -> ()
bar = undefined

foo1 :: forall l1 l2. Proxy (l1 :: [Type]) -> Proxy (l2 :: [Type]) -> ()
foo1 _ _ = bar (Proxy @(Append '[Int, Bool] l2)) (Proxy @(Append '[Int, Bool] _))

foo2 :: forall l1 l2. Proxy (l1 :: [Type]) -> Proxy (l2 :: [Type]) -> ()
foo2 _ _ = bar (Proxy @(Append l1 l2)) (Proxy @(Append l1 _))