Implement product of datatypes in generics-sop: liftA2 (++) of codes

Product_of_Codes.hs

-- This witnesses multiplying two polynomials
-- 
--   Code (Maybe a) = [[], [a]]
--   Code (Maybe b) = [[], [b]]
-- 
-- Then the product of (Maybe a, Maybe b) is isomorphic to the
-- multiplication of their codes
-- 
--   Code (MegaMaybe a b) = [[], [a], [b], [a,b]]
-- 
-- With unit 
-- 
--   Code () = [[]]
-- 
-- serving as identity
-- 
--   >> () × LT :: Ordering
--   LT
--   >> () × EQ :: Ordering
--   EQ
--   >> () × GT :: Ordering
--   GT
--   >> LT × () :: Ordering
--   LT
--   >> EQ × () :: Ordering
--   EQ
--   >> GT × () :: Ordering
--   GT
--
-- The operation of multiplication is equivalent to
-- 
--   liftA2 @[] (++) 
--
-- where 
-- 
--   liftA2 (++) []     _  = []
--   liftA2 (++) (a:as) bs = fmap (as ++) bs ++ liftA2 (++) as bs
--
-- And thus this gist defines a code that maps
-- 
--   SOP I ass -> SOP I bss -> SOP I (liftA2 (++) ass bss)
-- 
-- except implemented with type families. 
-- 
--   >> (1, 2, 3) × () :: (Int, Int, Int)
--   (1,2,3)
--   >> (1, 2, 3) × Solo 4 :: (Int, Int, Int, Int)
--   (1,2,3,4)
--   >> (1, 2, 3) × (4, 5) :: (Int, Int, Int, Int, Int)
--   (1,2,3,4,5)
--   >> (1, 2, 3) × (4, 5, 6) :: (Int, Int, Int, Int, Int, Int)
--   (1,2,3,4,5,6)
--   >> (1, 2, 3) × (4, 5, 6, 7) :: (Int, Int, Int, Int, Int, Int, Int)
--   (1,2,3,4,5,6,7)

{-# Language AllowAmbiguousTypes      #-}
{-# Language BlockArguments           #-}
{-# Language DataKinds                #-}
{-# Language DeriveAnyClass           #-}
{-# Language DeriveGeneric            #-}
{-# Language DerivingStrategies       #-}
{-# Language FlexibleContexts         #-}
{-# Language GADTs                    #-}
{-# Language ImportQualifiedPost      #-}
{-# Language InstanceSigs             #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}
{-# Language TypeFamilies             #-}
{-# Language TypeOperators            #-}
{-# Language UndecidableInstances     #-}

import Data.Kind
import Generics.SOP
import Generics.SOP qualified as SOP
import Unsafe.Coerce
import GHC.Generics qualified as GHC

-- >> Nothing × Nothing :: MegaMaybe _ _
-- None
-- >> Nothing × Just 2 :: MegaMaybe _ _
-- Some1 2
-- >> Just 1 × Nothing :: MegaMaybe _ _
-- Some2 1
-- >> Just 1 × Just 2 :: MegaMaybe _ _
-- Some12 1 2
type MegaMaybe :: Type -> Type -> Type
data MegaMaybe a b = None | Some1 a | Some2 b | Some12 a b
  deriving 
  stock (Show, GHC.Generic)

  deriving
  anyclass SOP.Generic

-- >> False × False :: MegaBool
-- FF
-- >> False × True :: MegaBool
-- FT
-- >> True × False :: MegaBool
-- TF
-- >> True × True :: MegaBool
-- TT
type MegaBool :: Type
data MegaBool = FF | FT | TF | TT
  deriving 
  stock (Show, GHC.Generic)

  deriving
  anyclass SOP.Generic

(×) :: (LiftAppendContraint (Code a1) (Code a2), LiftAppendC (Code a1), Generic a3, Generic a1, Generic a2, Code a3 ~ LiftAppend (Code a1) (Code a2)) => a1 -> a2 -> a3
as × bs = 
 to do
  SOP do
   liftAppendC 
    do unSOP (from as) 
    do unSOP (from bs)

--   liftA2 (++) (as:ass) bss
-- = map (as ++) bss ++ liftA2 (++) ass bss
type 
  LiftAppend :: [[k]] -> [[k]] -> [[k]]
type family
  LiftAppend ass bss where
  LiftAppend '[]      _   = '[]
  LiftAppend (as:ass) bss = MapAppend as bss ++ LiftAppend ass bss

type  LiftAppendC :: [[k]] -> Constraint
class LiftAppendC (ass :: [[k]]) where
  type LiftAppendContraint ass (bss :: [[k]]) :: Constraint

  liftAppendC :: LiftAppendContraint ass bss => NS (NP f) ass -> NS (NP f) bss -> NS (NP f) (LiftAppend ass bss)

instance LiftAppendC '[] where
  type LiftAppendContraint '[] bss = ()
  liftAppendC :: NS (NP f) '[] -> NS (NP f) bss -> NS (NP f) '[]
  liftAppendC = const

instance LiftAppendC ass => LiftAppendC (as:ass) where
  type LiftAppendContraint (as:ass) bss = (MapAppendC bss, MapAppendConstraint as bss, LiftAppendContraint ass bss, LengthC (MapAppend as bss))
  liftAppendC :: forall f bss. MapAppendC bss => MapAppendConstraint as bss => LiftAppendContraint ass bss => LengthC (MapAppend as bss) => NS (NP f) (as:ass) -> NS (NP f) bss -> NS (NP f) (MapAppend as bss ++ LiftAppend ass bss)
  liftAppendC (Z as) bss = shiftNS' @_ @_ @(LiftAppend ass bss) x where

    x :: NS (NP f) (MapAppend as bss)
    x = mapAppendC as bss

  liftAppendC (S ass) bss = shiftNS len (liftAppendC ass bss) where

    len :: Length (MapAppend as bss)
    len = lengthC

type  LengthC :: [k] -> Constraint
class LengthC as where
  lengthC :: Length as

instance LengthC '[] where
  lengthC :: Length '[]
  lengthC = LZ

instance LengthC as => LengthC (a:as) where
  lengthC :: Length (a:as)
  lengthC = LS lengthC

type Length :: [k] -> Type
data Length as where
  LZ :: Length '[]
  LS :: Length as -> Length (a:as)

shiftNS' :: NS f as -> NS f (as ++ suffix)
shiftNS' = unsafeCoerce

shiftNS :: forall prefix f as. Length prefix -> NS f as -> NS f (prefix ++ as)
shiftNS prefix = go LZ where

  go :: forall locals. Length locals -> NS f (locals ++ as) -> NS f (locals ++ prefix ++ as)
  go LZ       ns        = weakenNS prefix ns
  go (LS len) (Z local) = Z local
  go (LS len) (S as)    = S (go len as) 


weakenNS :: Length prefix -> NS f xs -> NS f (prefix ++ xs)
weakenNS LZ       sum = sum
weakenNS (LS len) sum = S (weakenNS len sum)


-- map (as ++) bss
type
  MapAppend :: [k] -> [[k]] -> [[k]]
type family
  MapAppend as bss where
  MapAppend _  '[]      = '[]
  MapAppend as (bs:bss) = (as ++ bs) : MapAppend as bss

type  MapAppendC :: [[k]] -> Constraint
class MapAppendC (bss :: [[k]]) where
  type MapAppendConstraint (as :: [k]) (bss :: [[k]]) :: Constraint

  mapAppendC 
    :: MapAppendConstraint as bss 
    => NP f as 
    -> NS (NP f) bss 
    -> NS (NP f) (MapAppend as bss)

instance MapAppendC '[] where
  type MapAppendConstraint as '[] = ()

  mapAppendC :: NP f as -> NS (NP f) '[] -> NS (NP f) '[]
  mapAppendC = const id

instance MapAppendC bss => MapAppendC (bs:bss) where
  type MapAppendConstraint as (bs:bss) = (AppendProdC as, MapAppendConstraint as bss)

  mapAppendC 
    :: forall as f. ()
    => AppendProdC as
    => MapAppendConstraint as bss
    => NP f as 
    -> NS (NP f) (bs:bss) 
    -> NS (NP f) ((as ++ bs) : MapAppend as bss)
  mapAppendC as (Z bs) = Z cs where

    cs :: NP f (as ++ bs)
    cs = appendProdC as bs

  mapAppendC as (S bs) = S cs where
    
    cs :: NS (NP f) (MapAppend as bss)
    cs = mapAppendC @_ @bss @as @f as bs

-- (++)
infixr 5 ++

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

type  AppendProdC :: [k] -> Constraint
class AppendProdC as where
  appendProdC :: NP f as -> NP f bs -> NP f (as ++ bs)

instance AppendProdC '[] where
  appendProdC :: NP f '[] -> NP f bs -> NP f bs
  appendProdC = const id

instance AppendProdC as => AppendProdC (a:as) where
  appendProdC :: NP f (a:as) -> NP f bs -> NP f (a:as ++ bs)
  appendProdC (a :* as) bs = a :* appendProdC as bs