Zero-cost overriding

Overriding.hs

{-# Language DerivingVia #-}
{-# Language StandaloneKindSignatures #-}
-- Some imports and pragmas missing.

import GHC.Generics
import Control.Applicative
import GHC.TypeLits
import Data.Kind
import Data.Coerce
import Data.Monoid

-- |
-- | Examples
-- |
data Progress = Progress
  { waiting   :: Int
  , submitted :: Int
  , started   :: Int
  , finished  :: Int
  , retried   :: Int
  }
  deriving stock (Eq, Ord, Show, Read, Generic)
  deriving (Semigroup, Monoid)
    via Overriding Progress '[ '[Sum Int, Sum Int, Sum Int, Sum Int, Sum Int] ]

data Misc a = Misc
  { one   :: Int
  , two   :: Bool -> Bool
  , three :: a
  }
  deriving stock Generic
  deriving (Semigroup, Monoid)
    via Overriding (Misc a)
      '[ '[Sum Int, Endo Bool, Sum a] ]

-- |
-- | Over-riding the Generic Rep, with SOP-style Code.
-- |
type    Override :: Type -> Code -> Type
newtype Override a code = Override { getOverride :: a }

instance (Generic a, forall x. CoercibleRep code a x) => Generic (Override a code) where
  type Rep (Override a code) = Apply code (Rep a)
  from :: forall x. Override a code -> Apply code (Rep a) x
  from = go . from . getOverride where
    go :: CoercibleRep code a x => Rep a x -> Apply code (Rep a) x
    go = coerce
  to :: forall x. Apply code (Rep a) x -> Override a code
  to = Override . to . go where
    go :: CoercibleRep code a x => Apply code (Rep a) x -> Rep a x
    go = coerce

type Overriding :: Type -> Code -> Type
type Overriding a code = Generically (Override a code)

type Code :: Type
type Code = [[Type]]

type
  Count :: (k -> Type) -> Nat
type family
  Count rep where
  Count U1             = 0
  Count (S1 meta rep)  = 1
  Count (rep :*: rep1) = Count rep + Count rep1

type
  Take :: Nat -> [k] -> [k]
type family
  Take n as where
  Take 0 _      = '[]
  Take n '[]    = '[]
  Take n (a:as) = a : Take (n - 1) as

type
  Drop :: Nat -> [k] -> [k]
type family
  Drop n as where
  Drop 0 as     = as
  Drop n '[]    = '[]
  Drop n (_:as) = Drop (n - 1) as

type
  Apply :: Code -> (k -> Type) -> (k -> Type)
type family
  Apply code rep where
  Apply code (D1 meta rep)  = D1 meta (Apply code rep)
  -- | The interesting cases are the binary constructors. The
  -- structure of a Generic Rep is not necessarily linear, it can
  -- nest.
  --
  --   data X a = X           -- U1
  --   data X a = X a         -- a
  --   data X a = X a a       -- a :*: a
  --   data X a = X a a a     -- a :*: (a :*: a)
  --   data X a = X a a a a   -- (a :*: a) :*: (a :*: a)
  --   data X a = X a a a a a -- (a :*: a) :*: (a :*: (a :*: a))
  --
  -- Passing the constructor code '[x,y,z,j,i] doesn't know how many
  -- fields the LHS takes versus the RHS, so we Count the number of
  -- fields and split the Code the gets passed to the first and second argument.
  --
  --   code
  -- = [x,    y,      z,     j,    i ]
  --
  --   take n code   drop n code
  -- = [x,    y]   = [z,     j,    i ]
  --   ^^^^^^^^^     ^^^^^^^^^^^^^^^^^
  --   (a :+: a) :*: (a :+: (a :+: a))
  --
  Apply code (rep :+: rep1) = Apply (Take (Count rep) code) rep :+: Apply (Drop (Count rep) code) rep1
  Apply '[] V1             = V1
  Apply '[constr] (C1 meta rep)  = C1 meta (ApplyConstr constr rep)

type
  ApplyConstr :: [Type] -> (k -> Type) -> (k -> Type)
type family
  ApplyConstr constr rep where
  ApplyConstr constr (rep :*: rep1) =
    ApplyConstr (Take (Count rep) constr) rep :*: ApplyConstr (Drop (Count rep) constr) rep1
  ApplyConstr '[] U1 = U1
  ApplyConstr '[val] (S1 meta rep) = S1 meta (ApplyValue val rep)

type
  ApplyValue :: Type -> (k -> Type) -> (k -> Type)
type family
  ApplyValue val rep where
  ApplyValue val (Rec0 _) = Rec0 val

class    Coercible (Rep a x) (Apply code (Rep a) x) => CoercibleRep code a x
instance Coercible (Rep a x) (Apply code (Rep a) x) => CoercibleRep code a x