    {-# LANGUAGE
        AllowAmbiguousTypes,
        DataKinds,
        FlexibleContexts,
        FlexibleInstances,
        MultiParamTypeClasses,
        PolyKinds,
        ScopedTypeVariables,
        TypeFamilies,
        TypeOperators,
        UndecidableInstances #-}

    -- | Surgeries that are just 'coerce'.
    --
    -- === Warning
    --
    -- This is an internal module: it is not subject to any versioning policy,
    -- breaking changes can happen at any time.
    --
    -- If something here seems useful, please report it or create a pull request to
    -- export it from an external module.

    module Generic.Data.Internal.Microsurgery where

    import Data.Coerce (Coercible, coerce)
    import Data.Kind (Type)
    import GHC.Generics
    import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)

    import Generic.Data.Types (Data)
    import Generic.Data.Internal.Generically (Generically(..), GenericProduct(..))

    -- * Surgery

    -- | Apply a microsurgery @s@ to a type @a@ for @DerivingVia@.
    --
    -- For the 'Data.Monoid.Monoid' class, see 'ProductSurgery'.
    --
    -- === Example
    --
    -- @
    -- {-\# LANGUAGE DerivingVia \#-}
    --
    -- -- The constructors must be visible.
    -- import "Generic.Data.Microsurgery"
    --   ('Surgery', 'Surgery''(..), 'Generically'(..), 'Derecordify')
    --
    -- data T = T { unT :: Int }
    --   deriving 'Show' via ('Surgery' 'Derecordify' T)
    --
    -- -- T won't be shown as a record:
    -- --   show (T {unT = 3}) == "T 3"
    -- @
    type Surgery (s :: Type) (a :: Type) = Generically (Surgery' s a)

    -- | Apply a microsurgery @s@ to a type @a@ for @DerivingVia@ for the
    -- 'Data.Monoid.Monoid' class.
    type ProductSurgery (s :: Type) (a :: Type) = GenericProduct (Surgery' s a)

    -- | Plural of 'Surgery'. Apply a list of microsurgeries.
    type Surgeries (s :: [Type]) (a :: Type) = Surgery (Cat s) a

    -- | Plural of 'ProductSurgery'. Apply a list of microsurgeries.
    type ProductSurgeries (s :: [Type]) (a :: Type) = ProductSurgery (Cat s) a

    -- | See 'Surgery'.
    newtype Surgery' (s :: Type) (a :: Type) = Surgery' { forall s a. Surgery' s a -> a
    unSurgery' :: a }

    instance (Generic a, Coercible (GSurgery s (Rep a)) (Rep a)) => Generic (Surgery' s a) where
      type Rep (Surgery' s a) = GSurgery s (Rep a)
      from :: forall x. Surgery' s a -> Rep (Surgery' s a) x
    from = ((a -> Rep a x) -> Surgery' s a -> GSurgery s (Rep a) x
    forall {x}. (a -> Rep a x) -> Surgery' s a -> GSurgery s (Rep a) x
    forall a b. Coercible a b => a -> b
    coerce :: forall x. (a -> Rep a x) -> Surgery' s a -> GSurgery s (Rep a) x) a -> Rep a x
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    from
      to :: forall x. Rep (Surgery' s a) x -> Surgery' s a
    to = ((Rep a x -> a) -> GSurgery s (Rep a) x -> Surgery' s a
    forall {x}. (Rep a x -> a) -> GSurgery s (Rep a) x -> Surgery' s a
    forall a b. Coercible a b => a -> b
    coerce :: forall x. (Rep a x -> a) -> GSurgery s (Rep a) x -> Surgery' s a) Rep a x -> a
    forall a x. Generic a => Rep a x -> a
    forall x. Rep a x -> a
    to

    -- | Apply a microsurgery represented by a symbol @s@ (declared as a dummy data
    -- type) to a generic representation @f@.
    type family GSurgery (s :: Type) (f :: k -> Type) :: k -> Type

    -- * Derecordify

    derecordify ::
      Coercible (GSurgery Derecordify f) f =>
      -- Coercible is not symmetric!??
      Data f p -> Data (GSurgery Derecordify f) p
    derecordify :: forall (f :: * -> *) p.
    Coercible (GSurgery Derecordify f) f =>
    Data f p -> Data (GSurgery Derecordify f) p
    derecordify = Data f p -> Data (GDerecordify f) p
    Data f p -> Data (GSurgery Derecordify f) p
    forall a b. Coercible a b => a -> b
    coerce

    underecordify ::
      Coercible f (GSurgery Derecordify f) =>
      Data (GSurgery Derecordify f) p -> Data f p
    underecordify :: forall (f :: * -> *) p.
    Coercible f (GSurgery Derecordify f) =>
    Data (GSurgery Derecordify f) p -> Data f p
    underecordify = Data (GDerecordify f) p -> Data f p
    Data (GSurgery Derecordify f) p -> Data f p
    forall a b. Coercible a b => a -> b
    coerce

    -- | Forget that a type was declared using record syntax.
    --
    -- > data Foo = Bar { baz :: Zap }
    -- >
    -- > -- becomes --
    -- >
    -- > data Foo = Bar Zap
    --
    -- Concretely, set the last field of 'MetaCons' to 'False' and forget field
    -- names.
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    data Derecordify :: Type
    type instance GSurgery Derecordify f = GDerecordify f

    type family GDerecordify (f :: k -> Type) :: k -> Type
    type instance GDerecordify (M1 D m f) = M1 D m (GDerecordify f)
    type instance GDerecordify (f :+: g) = GDerecordify f :+: GDerecordify g
    type instance GDerecordify (f :*: g) = GDerecordify f :*: GDerecordify g
    type instance GDerecordify (M1 C ('MetaCons nm fx _isRecord) f) = M1 C ('MetaCons nm fx 'False) (GDerecordify f)
    type instance GDerecordify (M1 S ('MetaSel _nm su ss ds) f) = M1 S ('MetaSel 'Nothing su ss ds) f
    type instance GDerecordify V1 = V1
    type instance GDerecordify U1 = U1

    -- * Type aging ("denewtypify")

    typeage ::
      Coercible (GSurgery Typeage f) f =>
      Data f p -> Data (GSurgery Typeage f) p
    typeage :: forall (f :: * -> *) p.
    Coercible (GSurgery Typeage f) f =>
    Data f p -> Data (GSurgery Typeage f) p
    typeage = Data f p -> Data (GSurgery Typeage f) p
    forall a b. Coercible a b => a -> b
    coerce

    untypeage ::
      Coercible f (GSurgery Typeage f) =>
      Data (GSurgery Typeage f) p -> Data f p
    untypeage :: forall (f :: * -> *) p.
    Coercible f (GSurgery Typeage f) =>
    Data (GSurgery Typeage f) p -> Data f p
    untypeage = Data (GSurgery Typeage f) p -> Data f p
    forall a b. Coercible a b => a -> b
    coerce

    -- | Forget that a type is a @newtype@. (The pun is that \"aging\" a type makes
    -- it no longer \"new\".)
    --
    -- > newtype Foo = Bar Baz
    -- >
    -- > -- becomes --
    -- >
    -- > data Foo = Bar Baz
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    data Typeage :: Type
    type instance GSurgery Typeage (M1 D ('MetaData nm md pk _nt) f) = M1 D ('MetaData nm md pk 'False) f

    -- * Renaming

    renameFields ::
      forall rnm f p.
      Coercible (GSurgery (RenameFields rnm) f) f =>
      Data f p -> Data (GSurgery (RenameFields rnm) f) p
    renameFields :: forall rnm (f :: * -> *) p.
    Coercible (GSurgery (RenameFields rnm) f) f =>
    Data f p -> Data (GSurgery (RenameFields rnm) f) p
    renameFields = Data f p -> Data (GRenameFields rnm f) p
    Data f p -> Data (GSurgery (RenameFields rnm) f) p
    forall a b. Coercible a b => a -> b
    coerce

    unrenameFields ::
      forall rnm f p.
      Coercible (GSurgery (RenameFields rnm) f) f =>
      Data f p -> Data (GSurgery (RenameFields rnm) f) p
    unrenameFields :: forall rnm (f :: * -> *) p.
    Coercible (GSurgery (RenameFields rnm) f) f =>
    Data f p -> Data (GSurgery (RenameFields rnm) f) p
    unrenameFields = Data f p -> Data (GRenameFields rnm f) p
    Data f p -> Data (GSurgery (RenameFields rnm) f) p
    forall a b. Coercible a b => a -> b
    coerce

    renameConstrs ::
      forall rnm f p.
      Coercible (GSurgery (RenameConstrs rnm) f) f =>
      Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    renameConstrs :: forall rnm (f :: * -> *) p.
    Coercible (GSurgery (RenameConstrs rnm) f) f =>
    Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    renameConstrs = Data f p -> Data (GRenameConstrs rnm f) p
    Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    forall a b. Coercible a b => a -> b
    coerce

    unrenameConstrs ::
      forall rnm f p.
      Coercible (GSurgery (RenameConstrs rnm) f) f =>
      Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    unrenameConstrs :: forall rnm (f :: * -> *) p.
    Coercible (GSurgery (RenameConstrs rnm) f) f =>
    Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    unrenameConstrs = Data f p -> Data (GRenameConstrs rnm f) p
    Data f p -> Data (GSurgery (RenameConstrs rnm) f) p
    forall a b. Coercible a b => a -> b
    coerce

    -- | Rename fields using the function @rnm@ given as a parameter.
    --
    -- > data Foo = Bar { baz :: Zap }
    -- >
    -- > -- becomes, renaming "baz" to "bag" --
    -- >
    -- > data Foo = Bar { bag :: Zap }
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    data RenameFields (rnm :: Type) :: Type
    type instance GSurgery (RenameFields rnm) f = GRenameFields rnm f

    type family GRenameFields (rnm :: Type) (f :: k -> Type) :: k -> Type
    type instance GRenameFields rnm (M1 D m f) = M1 D m (GRenameFields rnm f)
    type instance GRenameFields rnm (f :+: g) = GRenameFields rnm f :+: GRenameFields rnm g
    type instance GRenameFields rnm (f :*: g) = GRenameFields rnm f :*: GRenameFields rnm g
    type instance GRenameFields rnm (M1 C m f) = M1 C m (GRenameFields rnm f)
    type instance GRenameFields rnm (M1 S ('MetaSel ('Just nm) su ss ds) f) = M1 S ('MetaSel ('Just (rnm @@ nm)) su ss ds) f
    type instance GRenameFields rnm V1 = V1
    type instance GRenameFields rnm U1 = U1

    -- | Rename constructors using the function @rnm@ given as a parameter.
    --
    -- > data Foo = Bar { baz :: Zap }
    -- >
    -- > -- becomes, renaming "Bar" to "Car" --
    -- >
    -- > data Foo = Car { baz :: Zap }
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    data RenameConstrs (rnm :: Type) :: Type
    type instance GSurgery (RenameConstrs rnm) f = GRenameConstrs rnm f

    type family GRenameConstrs (rnm :: Type) (f :: k -> Type) :: k -> Type
    type instance GRenameConstrs rnm (M1 D m f) = M1 D m (GRenameConstrs rnm f)
    type instance GRenameConstrs rnm (f :+: g) = GRenameConstrs rnm f :+: GRenameConstrs rnm g
    type instance GRenameConstrs rnm (f :*: g) = GRenameConstrs rnm f :*: GRenameConstrs rnm g
    type instance GRenameConstrs rnm (M1 C ('MetaCons nm fi ir) f) = M1 C ('MetaCons (rnm @@ nm) fi ir) f
    type instance GRenameConstrs rnm V1 = V1

    -- ** Defining symbol functions

    -- | @f \@\@ s@ is the application of a type-level function symbolized by @f@
    -- to a @s :: 'Symbol'@.
    --
    -- A function @FooToBar@ can be defined as follows:
    --
    -- @
    -- data FooToBar
    -- type instance FooToBar '@@' \"foo\" = \"bar\"
    -- @
    type family (f :: Type) @@ (s :: Symbol) :: Symbol

    -- | Identity function @'Symbol' -> 'Symbol'@.
    data SId
    type instance SId @@ s = s

    -- | Empty function (compile-time error when applied).
    data SError
    type instance SError @@ s = TypeError ('Text "Invalid name: " ':<>: 'ShowType s)

    -- | Constant function.
    data SConst (s :: Symbol)
    type instance SConst z @@ _s = z

    -- | Define a function for a fixed set of strings, and fall back to @f@ for the others.
    data SRename (xs :: [(Symbol, Symbol)]) (f :: Type)
    type instance SRename xs f @@ s = SRename' xs f s

    -- | Closed type family for 'SRename'.
    type family SRename' (xs :: [(Symbol, Symbol)]) (f :: Type) (s :: Symbol) where
      SRename' '[] f s = f @@ s
      SRename' ('( s,  t) ': _xs) _f s = t
      SRename' ('(_r, _t) ':  xs)  f s = SRename' xs f s

    -- * Other

    -- This can be used with generic-lens (see Generic.Data.Microsurgery)

    -- | Unify the "spines" of two generic representations (the "spine" is
    -- everything except the field types).
    class UnifyRep (f :: k -> Type) (g :: k -> Type)
    instance (g' ~ M1 s c g, UnifyRep f g) => UnifyRep (M1 s c f) g'
    instance (g' ~ (g1 :+: g2), UnifyRep f1 g1, UnifyRep f2 g2)
      => UnifyRep (f1 :+: f2) g'
    instance (g' ~ (g1 :*: g2), UnifyRep f1 g1, UnifyRep f2 g2)
      => UnifyRep (f1 :*: f2) g'
    instance (g' ~ K1 i b) => UnifyRep (K1 i a) g'
    instance (g' ~ U1) => UnifyRep U1 g'
    instance (g' ~ V1) => UnifyRep V1 g'

    -- |
    --
    -- > onData :: _ => (Data r x -> Data s y) -> (Data r x -> Data s y)  -- possible specialization
    --
    -- Can be used with @generic-lens@ for type-changing field updates with @field_@
    -- (and possibly other generic optics).
    --
    -- A specialization of the identity function to be used to fix types
    -- of functions on 'Data', unifying the "spines" of input and output generic
    -- representations (the "spine" is everything except field types, which may
    -- thus change).
    onData
      :: (UnifyRep r s, UnifyRep s r)
      => p (Data r x) (Data s y) -> p (Data r x) (Data s y)
    onData :: forall (r :: * -> *) (s :: * -> *) (p :: * -> * -> *) x y.
    (UnifyRep r s, UnifyRep s r) =>
    p (Data r x) (Data s y) -> p (Data r x) (Data s y)
    onData = p (Data r x) (Data s y) -> p (Data r x) (Data s y)
    forall a. a -> a
    id

    -- | Apply a type constructor @f@ to every field type of a generic
    -- representation @r@.
    --
    -- > data Color = RGB
    -- >   { r :: Int
    -- >   , g :: Int
    -- >   , b :: Int }
    -- >
    -- > -- becomes --
    -- >
    -- > data Color f = RGB
    -- >   { r :: f Int
    -- >   , g :: f Int
    -- >   , b :: f Int }
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    data OnFields (f :: Type -> Type) :: Type
    type instance GSurgery (OnFields f) g = GOnFields f g

    type family GOnFields (f :: Type -> Type) (g :: k -> Type) :: k -> Type
    type instance GOnFields f (M1 s m r) = M1 s m (GOnFields f r)
    type instance GOnFields f (r :+: s) = GOnFields f r :+: GOnFields f s
    type instance GOnFields f (r :*: s) = GOnFields f r :*: GOnFields f s
    type instance GOnFields f (K1 i a) = K1 i (f a)
    type instance GOnFields f U1 = U1
    type instance GOnFields f V1 = V1

    -- | Apply a type constructor @f@ to every field type of a type @a@ to make a
    -- synthetic type.
    type DOnFields (f :: Type -> Type) (a :: Type) = Data (GSurgery (OnFields f) (Rep a)) ()

    -- | Apply a type constructor @f@ to the field named @s@ in a generic record @r@.
    --
    -- > data Vec a = Vec
    -- >   { len :: Int
    -- >   , contents :: [a] }
    -- >
    -- > -- with (OnField "len" Sum) becomes --
    -- >
    -- > data Vec a = Vec
    -- >   { len :: Sum Int
    -- >   , contents :: [a] }
    --
    -- This is a defunctionalized symbol, applied using 'GSurgery' or 'Surgery'.
    -- See also the synonym @('%~')@.
    data OnField (s :: Symbol) (f :: Type -> Type) :: Type
    type instance GSurgery (OnField s f) g = GOnField s f g

    type family GOnField (x :: Symbol) (f :: Type -> Type) (g :: k -> Type) :: k -> Type where
      GOnField x f (M1 S ('MetaSel ('Just x) a b c) (K1 i t)) = M1 S ('MetaSel ('Just x) a b c) (K1 i (f t))
      GOnField x f (M1 S m r) = M1 S m r
      GOnField x f (M1 C m r) = M1 C m (GOnField x f r)
      GOnField x f (M1 D m r) = M1 D m (GOnField x f r)
      GOnField x f (r :+: s) = GOnField x f r :+: GOnField x f s
      GOnField x f (r :*: s) = GOnField x f r :*: GOnField x f s
      GOnField x f (K1 i a) = K1 i (f a)
      GOnField x f U1 = U1
      GOnField x f V1 = V1

    -- | Infix name for 'OnField'. To be used with 'Surgeries' or 'Cat'.
    --
    -- === __Examples__
    --
    -- Transform one @Int@ field into @'Data.Monoid.Sum' Int@ for deriving 'Monoid':
    --
    -- @
    -- data Vec a = Vec
    --   { len :: Int
    --   , contents :: [a] }
    --   deriving Generic
    --   deriving (Eq, Show) via Generically (Vec a)
    --   deriving (Semigroup, Monoid) via 'ProductSurgeries' '[\"len\" '%~' 'Data.Monoid.Sum'] (Vec a)
    -- @
    --
    -- Wrap unshowable fields in 'Generic.Data.Opaque' for deriving 'Show':
    --
    -- @
    -- data Unshowable = Unshowable
    --   { fun :: Int -> Int
    --   , io :: IO Bool
    --   , int :: Int }
    --   deriving Generic
    --   deriving Show via 'Surgeries' '[\"fun\" '%~' 'Generic.Data.Opaque', \"io\" '%~' 'Generic.Data.Opaque'] Unshowable
    --
    -- -- show (Unshowable id (pure True) 42) = \"Unshowable _ _ 42\"
    -- @
    type (%~) = OnField
    infixr 4 %~

    -- | Compose surgeries together.
    data Cat (ss :: [Type]) :: Type
    type instance GSurgery (Cat '[]) g = g
    type instance GSurgery (Cat (s ': ss)) g = GSurgery s (GSurgery (Cat ss) g)

    -- | Make a synthetic type ('Data') by chaining multiple surgeries.
    type DCat (ss :: [Type]) (a :: Type) = Data (GSurgery (Cat ss) (Rep a)) ()

    -- | Change the generic representation to that of another type @a@.
    data CopyRep (a :: Type) :: Type
    type instance GSurgery (CopyRep a) _ = Rep a

    copyRep :: forall a f p.
      Coercible (GSurgery (CopyRep a) f) f =>
      Data f p -> Data (GSurgery (CopyRep a) f) p
    copyRep :: forall a (f :: * -> *) p.
    Coercible (GSurgery (CopyRep a) f) f =>
    Data f p -> Data (GSurgery (CopyRep a) f) p
    copyRep = Data f p -> Data (Rep a) p
    Data f p -> Data (GSurgery (CopyRep a) f) p
    forall a b. Coercible a b => a -> b
    coerce

    uncopyRep :: forall a f p.
      Coercible f (GSurgery (CopyRep a) f) =>
      Data (GSurgery (CopyRep a) f) p -> Data f p
    uncopyRep :: forall a (f :: * -> *) p.
    Coercible f (GSurgery (CopyRep a) f) =>
    Data (GSurgery (CopyRep a) f) p -> Data f p
    uncopyRep = Data (Rep a) p -> Data f p
    Data (GSurgery (CopyRep a) f) p -> Data f p
    forall a b. Coercible a b => a -> b
    coerce