Illegal type synonym family in instance - Haskell

{-# LANGUAGE TypeFamilies, FunctionalDependencies, LambdaCase #-}
module SOP.Sums where

import MyPrelude

import GHC.Generics

import Data.Void

import Optics

type family Sum (xs :: [*]) :: *
  where
  Sum '[] = Void
  Sum (x ': xs) = Either x (Sum xs)

class Coproduct c xs | c -> xs
  where
  asCoproduct :: Iso' c (Sum xs)

instance Coproduct (U1 p) '[()]
  where
  asCoproduct = iso (\U1 -> Left ()) (either (const U1) absurd)

instance Coproduct (K1 i c p) '[c]
  where
  asCoproduct = iso (\(K1 c) -> Left c) (either K1 absurd)

instance (Functor f, Coproduct (f p) xs) => Coproduct (M1 i c f p) xs
  where
  asCoproduct = iso (\(M1 fp) -> fwd asCoproduct fp) (M1 . bwd asCoproduct)

type family xs ++ ys :: [*]
  where
  '[] ++ xs = xs
  (x ': xs) ++ ys = x ': (xs ++ys)

instance (Coproduct (f p) xs, Coproduct (g p) ys) => Coproduct ((f :+: g) p) (xs ++ ys)
  where
  asCoproduct = iso (\case { L1 fp -> Left fp; R1 gp -> Right $ fwd asCoproduct gp }) (either L1 (R1 . bwd asCoproduct))

[typecheck] [E] /mnt/data/depot/git/haskell/repos/co-optics/src/SOP/Sums.hs:38:54: error:
    • Illegal type synonym family application in instance: xs ++ ys
    • In the instance declaration for
        ‘Coproduct ((f :+: g) p) (xs ++ ys)’

class Append (xs :: [*]) (ys :: [*]) (zs :: [*]) | xs ys -> zs
  where
  appendCoproducts :: Proxy xs -> Proxy ys -> Either (Sum xs) (Sum ys) -> Sum zs

instance Append '[] ys ys
  where
  appendCoproducts _ _ = either absurd id

instance Append xs ys zs => Append (x ': xs) ys (x ': zs)
  where
  appendCoproducts (_ :: Proxy (x ': xs)) (_ :: Proxy ys) = either (either Left (\xs -> Right $ appendCoproducts (Proxy @xs) (Proxy @ys) $ Left xs)) (\ys -> Right $ appendCoproducts (Proxy @xs) (Proxy @ys) (Right ys))

instance (Coproduct (f p) xs, Coproduct (g p) ys, Append xs ys zs) => Coproduct ((f :+: g) p) zs
  where
  asCoproduct = iso _ _

class Append (xs :: [*]) (ys :: [*]) (zs :: [*]) | xs ys -> zs
  where
  (|||) :: Proxy xs -> Proxy ys -> Either (Sum xs) (Sum ys) -> Sum zs

instance Append '[] ys ys
  where
  _ ||| _ = either absurd id

instance Append xs ys zs => Append (x ': xs) ys (x ': zs)
  where
  (_ :: Proxy (x ': xs)) ||| (_ :: Proxy ys) = either (either Left (\xs -> Right $ (Proxy @xs ||| Proxy @ys) $ Left xs)) (\ys -> Right $ (Proxy @xs ||| Proxy @ys) (Right ys))

instance (Coproduct (f p) xs, Coproduct (g p) ys, Append xs ys zs) => Coproduct ((f :+: g) p) zs
  where
  asCoproduct = iso
    (\case { L1 fp  -> (Proxy @xs ||| Proxy @ys) $ Left $ fwd asCoproduct fp; R1 gp -> (Proxy @xs ||| Proxy @ys) $ Right $ fwd asCoproduct gp })
    _

class Coproduct' c rs xs where
  asCoproduct' :: Iso' (Either c (Sum rs)) (Sum xs)

class Append (xs :: [*]) (ys :: [*]) (zs :: [*]) | xs ys -> zs
  where
  (|||) :: Proxy xs -> Proxy ys -> Iso' (Either (Sum xs) (Sum ys)) (Sum zs)

instance Append '[] ys ys
  where
  _ ||| _ = iso (either absurd id) Right

instance Append xs ys zs => Append (x ': xs) ys (x ': zs)
  where
  (_ :: Proxy (x ': xs)) ||| (_ :: Proxy ys) = iso
    (either
      (either Left (Right . fwd (Proxy @xs ||| Proxy @ys) . Left))
      (Right . fwd (Proxy @xs ||| Proxy @ys) . Right))
    _