{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
{-# LANGUAGE KindSignatures, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications     #-}
module T13538 where

import GHC.TypeLits
import Data.Proxy

-- | Synonym for a type-level snoc (injective!)
type (ns :: [k]) +: (n :: k) = GetList1 (SinkFirst (n ': ns))
infixl 5 +:



-- | A weird data type used to make `(+:)` operation injective.
--   `List k [k]` must have at least two elements.
data List1 k = L1Single k | L1Head k [k]

-- | Sink first element of a list to the end of the list
type family SinkFirst (xs :: [k]) = (ys :: List1 k) | ys -> xs where
  SinkFirst '[y]       = 'L1Single y
  -- SinkFirst (y ': x ': xs :: [Nat])
  --     = ('L1Head x (GetList1Nat (SinkFirst (y ': xs))) :: List1 Nat)
  SinkFirst (y ': x ': xs :: [k])
      = ('L1Head x (GetList1    (SinkFirst (y ': xs))) :: List1 k)

type family GetList1 (ts :: List1 k) = (rs :: [k]) | rs -> ts where
  GetList1 ('L1Single x) = '[x]
  GetList1 ('L1Head y (x ':xs)) = y ': x ': xs
type family GetList1Nat (ts :: List1 Nat) = (rs :: [Nat]) | rs -> ts where
  GetList1Nat ('L1Single x) = '[x]
  GetList1Nat ('L1Head y (x ': xs)) = y ': x ': xs

type family (++) (as :: [k]) (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)


ff :: Proxy k -> Proxy (as +: k) -> Proxy (k ': bs) -> Proxy (as ++ bs)
ff _ _ _ = Proxy

yy :: Proxy '[3,7,2]
yy = ff (Proxy @5) (Proxy @'[3,7,5]) (Proxy @'[5,2])