A solution to https://www.reddit.com/r/haskell/comments/ob0a1a/type_level_concat_with_good_inference/

IConcat.hs

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

import           Data.Proxy

class InferRight (xs :: [a]) (ys :: [a]) (zs :: [a])
instance ys ~ zs => InferRight '[] ys zs
instance (zs ~ (x ': zs'), InferRight xs' ys zs') => InferRight (x ': xs') ys zs

-- We could inline that into `InferLeftSpine` if we were golfing, but having a separate definition is cleaner.
class SameSpineR (xs :: [a]) (zs :: [a])
instance xs ~ '[] => SameSpineR xs '[]
instance (xs ~ (x ': xs'), SameSpineR xs' zs') => SameSpineR xs (z ': zs')

class InferLeftSpine (xs :: [a]) (ys :: [a]) (zs :: [a])
instance SameSpineR xs zs => InferLeftSpine xs '[] zs
instance (zs ~ (z ': zs'), InferLeftSpine xs ys' zs') => InferLeftSpine xs (y ': ys') zs

type IConcat xs ys zs = (InferRight xs ys zs, InferLeftSpine xs ys zs)

l :: Proxy '[1,2]
l = Proxy

r :: Proxy '[3,4]
r = Proxy

cat :: IConcat a b c => Proxy a -> Proxy b -> Proxy c
cat _ _ = Proxy

c1 :: Proxy '[1,2,3,4]
c1 = cat l _
-- _ :: Proxy '[3,4]

c2 :: Proxy '[1,2,3,4]
c2 = cat _ r
-- _ :: Proxy '[1,2]
c3 = cat l r
-- c3 :: Proxy '[1,2,3,4]

Adding a bit of kind polymorphism should clarify things a little.

class SameSpineR (xs :: [a]) (zs :: [b])
instance xs ~ '[] => SameSpineR xs '[]
instance (xs ~ (x ': xs'), SameSpineR xs' zs') => SameSpineR xs (z ': zs')

class InferLeftSpine (xs :: [a]) (ys :: [b]) (zs :: [c])
instance SameSpineR xs zs => InferLeftSpine xs '[] zs
instance (zs ~ (z ': zs'), InferLeftSpine xs ys' zs') => InferLeftSpine xs (y ': ys') zs

True, that makes it much clearer.