Changing Generic representation, using SOP style Code

Overriding.hs

-- this allows you to derive
-- 
--   data OneTwo = OneTwo { x :: Int, y :: Int }
--     deriving stock Generic
--     deriving (Semigroup, Monoid) via Overriding '[ '[Sum Int, Sum Int] ] Onetwo

-- | Override
newtype Override (code :: [[Type]]) a = Override { getOverride :: a }

type Overriding code a = Generically (Override code a)

instance (Generic a, Ok NowSum code (Rep a)) => Generic (Override code a) where
  type Rep (Override code a) = New NowSum code (Rep a)

  from :: Override code a -> New NowSum code (Rep a) x
  from = ok @_ @NowSum @code . from . getOverride

  to :: New NowSum code (Rep a) x -> Override code a
  to = Override . to . ko @_ @NowSum @code

-- | Classes

type Now :: Type -> Type
data Now k where
  NowSum  :: Now [[Type]]
  NowProd :: Now  [Type]
  NowVal  :: Now   Type

type  Ok :: Now k -> k -> (Type -> Type) -> Constraint
class Ok now code old where
  type New now code old :: Type -> Type
  ok :: old ~> New now code old
  ko :: old <~ New now code old

-- | NowSum
instance Ok NowSum code old => Ok NowSum code (D1 meta old) where
  type New NowSum code (D1 meta old) = D1 meta (New NowSum code old)
  ok :: D1 meta old ~> D1 meta (New NowSum code old)
  ko :: D1 meta old <~ D1 meta (New NowSum code old)
  ok = M1 . ok @_ @NowSum @code . unM1
  ko = M1 . ko @_ @NowSum @code . unM1

instance (Ok NowSum '[c] old, Ok NowSum (c1:code) old1)
      => Ok NowSum (c:c1:code) (old :+: old1) where
  type New NowSum (c:c1:code) (old :+: old1) =
    New NowSum '[c] old :+: New NowSum (c1:code) old1
  ok :: (old :+: old1) ~> (New NowSum '[c] old :+: New NowSum (c1:code) old1)
  ko :: (old :+: old1) <~ (New NowSum '[c] old :+: New NowSum (c1:code) old1)
  ok (L1 old)  = L1 (ok @_ @NowSum @'[c] old)
  ok (R1 old1) = R1 (ok @_ @NowSum @(c1:code) old1)
  ko (L1 old)  = L1 (ko @_ @NowSum @'[c] old)
  ko (R1 old1) = R1 (ko @_ @NowSum @(c1:code) old1)

instance Ok NowSum '[] V1 where
  type New NowSum '[] V1 = V1
  ok, ko :: V1 ~> V1
  ok = id
  ko = id

instance Ok NowProd constr old => Ok NowSum '[constr] (C1 meta old) where
  type New NowSum '[constr] (C1 meta old) = C1 meta (New NowProd constr old)
  ok :: C1 meta old ~> C1 meta (New NowProd constr old)
  ko :: C1 meta old <~ C1 meta (New NowProd constr old)
  ok = M1 . ok @_ @NowProd @constr . unM1
  ko = M1 . ko @_ @NowProd @constr . unM1

-- | NowProd
instance Ok NowVal val old => Ok NowProd '[val] (S1 meta old) where
  type New NowProd '[val] (S1 meta old) = S1 meta (New NowVal val old)
  ok :: S1 meta old ~> S1 meta (New NowVal val old)
  ko :: S1 meta old <~ S1 meta (New NowVal val old)
  ok = M1 . ok @_ @NowVal @val . unM1
  ko = M1 . ko @_ @NowVal @val . unM1

instance (Ok NowProd '[val] old, Ok NowProd (val1:constr) old1)
      => Ok NowProd (val:val1:constr) (old :*: old1) where
  type New NowProd (val:val1:constr) (old :*: old1) =
    New NowProd '[val] old :*: New NowProd (val1:constr) old1
  ok :: (old :*: old1) ~> (New NowProd '[val] old :*: New NowProd (val1:constr) old1)
  ko :: (old :*: old1) <~ (New NowProd '[val] old :*: New NowProd (val1:constr) old1)
  ok (old :*: old1) = ok @_ @NowProd @'[val] old :*: ok @_ @NowProd @(val1:constr) old1
  ko (old :*: old1) = ko @_ @NowProd @'[val] old :*: ko @_ @NowProd @(val1:constr) old1

instance Ok NowProd '[] U1 where
  type New NowProd '[] U1 = U1
  ok :: U1 ~> U1
  ko :: U1 <~ U1
  ok = id
  ko = id

-- | NowVal
instance Coercible old new => Ok NowVal new (Rec0 old) where
  type New NowVal new (Rec0 old) = Rec0 new
  ok :: Rec0 old ~> Rec0 new
  ko :: Rec0 old <~ Rec0 new
  ok = coerce
  ko = coerce