    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE UndecidableSuperClasses #-}
    -- | Codes and interpretations
    module Generics.SOP.Universe where

    import Data.Kind (Type)
    import Data.Coerce (Coercible, coerce)
    import Data.Proxy
    import qualified GHC.Generics as GHC

    import Generics.SOP.BasicFunctors
    import Generics.SOP.Constraint
    import Generics.SOP.NP
    import Generics.SOP.NS
    import Generics.SOP.GGP
    import Generics.SOP.Metadata
    import qualified Generics.SOP.Type.Metadata as T

    -- | The (generic) representation of a datatype.
    --
    -- A datatype is isomorphic to the sum-of-products of its code.
    -- The isomorphism is witnessed by 'from' and 'to' from the
    -- 'Generic' class.
    --
    type Rep a = SOP I (Code a)

    -- | The class of representable datatypes.
    --
    -- The SOP approach to generic programming is based on viewing
    -- datatypes as a representation ('Rep') built from the sum of
    -- products of its components. The components of a datatype
    -- are specified using the 'Code' type family.
    --
    -- The isomorphism between the original Haskell datatype and its
    -- representation is witnessed by the methods of this class,
    -- 'from' and 'to'. So for instances of this class, the following
    -- laws should (in general) hold:
    --
    -- @
    -- 'to' '.' 'from' === 'id' :: a -> a
    -- 'from' '.' 'to' === 'id' :: 'Rep' a -> 'Rep' a
    -- @
    --
    -- You typically don't define instances of this class by hand, but
    -- rather derive the class instance automatically.
    --
    -- /Option 1:/ Derive via the built-in GHC-generics. For this, you
    -- need to use the @DeriveGeneric@ extension to first derive an
    -- instance of the 'GHC.Generics.Generic' class from module "GHC.Generics".
    -- With this, you can then give an empty instance for 'Generic', and
    -- the default definitions will just work. The pattern looks as
    -- follows:
    --
    -- @
    -- import qualified "GHC.Generics" as GHC
    -- import "Generics.SOP"
    --
    -- ...
    --
    -- data T = ... deriving (GHC.'GHC.Generics.Generic', ...)
    --
    -- instance 'Generic' T -- empty
    -- instance 'HasDatatypeInfo' T -- empty, if you want/need metadata
    -- @
    --
    -- /Option 2:/ Derive via Template Haskell. For this, you need to
    -- enable the @TemplateHaskell@ extension. You can then use
    -- 'Generics.SOP.TH.deriveGeneric' from module "Generics.SOP.TH"
    -- to have the instance generated for you. The pattern looks as
    -- follows:
    --
    -- @
    -- import "Generics.SOP"
    -- import "Generics.SOP.TH"
    --
    -- ...
    --
    -- data T = ...
    --
    -- 'Generics.SOP.TH.deriveGeneric' \'\'T -- derives 'HasDatatypeInfo' as well
    -- @
    --
    -- /Tradeoffs:/ Whether to use Option 1 or 2 is mainly a matter
    -- of personal taste. The version based on Template Haskell probably
    -- has less run-time overhead.
    --
    -- /Non-standard instances:/
    -- It is possible to give 'Generic' instances manually that deviate
    -- from the standard scheme, as long as at least
    --
    -- @
    -- 'to' '.' 'from' === 'id' :: a -> a
    -- @
    --
    -- still holds.
    --
    class (All SListI (Code a)) => Generic (a :: Type) where
      -- | The code of a datatype.
      --
      -- This is a list of lists of its components. The outer list contains
      -- one element per constructor. The inner list contains one element
      -- per constructor argument (field).
      --
      -- /Example:/ The datatype
      --
      -- > data Tree = Leaf Int | Node Tree Tree
      --
      -- is supposed to have the following code:
      --
      -- > type instance Code (Tree a) =
      -- >   '[ '[ Int ]
      -- >    , '[ Tree, Tree ]
      -- >    ]
      --
      type Code a :: [[Type]]
      type Code a = GCode a

      -- | Converts from a value to its structural representation.
      from         :: a -> Rep a
      default from :: (GFrom a, GHC.Generic a, Rep a ~ SOP I (GCode a))
                   => a -> Rep a
      from = a -> SOP I (GCode a)
    a -> Rep a
    forall a. (GFrom a, Generic a) => a -> SOP I (GCode a)
    gfrom

      -- | Converts from a structural representation back to the
      -- original value.
      to         :: Rep a -> a
      default to :: (GTo a, GHC.Generic a, Rep a ~ SOP I (GCode a))
                 => Rep a -> a
      to = SOP I (GCode a) -> a
    Rep a -> a
    forall a. (GTo a, Generic a) => SOP I (GCode a) -> a
    gto

    -- | A class of datatypes that have associated metadata.
    --
    -- It is possible to use the sum-of-products approach to generic programming
    -- without metadata. If you need metadata in a function, an additional
    -- constraint on this class is in order.
    --
    -- You typically don't define instances of this class by hand, but
    -- rather derive the class instance automatically. See the documentation
    -- of 'Generic' for the options.
    --
    class Generic a => HasDatatypeInfo a where
      -- | Type-level datatype info
      type DatatypeInfoOf a :: T.DatatypeInfo
      type DatatypeInfoOf a = GDatatypeInfoOf a

      -- | Term-level datatype info; by default, the term-level datatype info is produced
      -- from the type-level info.
      --
      datatypeInfo         :: proxy a -> DatatypeInfo (Code a)
      default datatypeInfo :: (GDatatypeInfo a, GCode a ~ Code a) => proxy a -> DatatypeInfo (Code a)
      datatypeInfo = proxy a -> DatatypeInfo (GCode a)
    proxy a -> DatatypeInfo (Code a)
    forall (proxy :: * -> *) a.
    GDatatypeInfo a =>
    proxy a -> DatatypeInfo (GCode a)
    gdatatypeInfo

    -- | Constraint that captures that a datatype is a product type,
    -- i.e., a type with a single constructor.
    --
    -- It also gives access to the code for the arguments of that
    -- constructor.
    --
    -- @since 0.3.1.0
    --
    type IsProductType (a :: Type) (xs :: [Type]) =
      (Generic a, Code a ~ '[ xs ])

    -- | Direct access to the part of the code that is relevant
    -- for a product type.
    --
    -- @since 0.4.0.0
    --
    type ProductCode (a :: Type) =
      Head (Code a)

    -- | Convert from a product type to its product representation.
    --
    -- @since 0.4.0.0
    --
    productTypeFrom :: IsProductType a xs => a -> NP I xs
    productTypeFrom :: forall a (xs :: [*]). IsProductType a xs => a -> NP I xs
    productTypeFrom = NS (NP I) '[xs] -> NP I xs
    forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
    unZ (NS (NP I) '[xs] -> NP I xs)
    -> (a -> NS (NP I) '[xs]) -> a -> NP I xs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP I '[xs] -> NS (NP I) '[xs]
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP (SOP I '[xs] -> NS (NP I) '[xs])
    -> (a -> SOP I '[xs]) -> a -> NS (NP I) '[xs]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SOP I '[xs]
    a -> Rep a
    forall a. Generic a => a -> Rep a
    from
    {-# INLINE productTypeFrom #-}

    -- | Convert a product representation to the original type.
    --
    -- @since 0.4.0.0
    --
    productTypeTo :: IsProductType a xs => NP I xs -> a
    productTypeTo :: forall a (xs :: [*]). IsProductType a xs => NP I xs -> a
    productTypeTo = SOP I '[xs] -> a
    Rep a -> a
    forall a. Generic a => Rep a -> a
    to (SOP I '[xs] -> a) -> (NP I xs -> SOP I '[xs]) -> NP I xs -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (NP I) '[xs] -> SOP I '[xs]
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NS (NP I) '[xs] -> SOP I '[xs])
    -> (NP I xs -> NS (NP I) '[xs]) -> NP I xs -> SOP I '[xs]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP I xs -> NS (NP I) '[xs]
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
    Z
    {-# INLINE productTypeTo #-}

    -- | Constraint that captures that a datatype is an enumeration type,
    -- i.e., none of the constructors have any arguments.
    --
    -- @since 0.3.1.0
    --
    type IsEnumType (a :: Type) =
      (Generic a, All ((~) '[]) (Code a))

    -- | Convert from an enum type to its sum representation.
    --
    -- @since 0.4.0.0
    --
    enumTypeFrom :: IsEnumType a => a -> NS (K ()) (Code a)
    enumTypeFrom :: forall a. IsEnumType a => a -> NS (K ()) (Code a)
    enumTypeFrom = (forall (a :: [*]). NP I a -> K () a)
    -> NS (NP I) (Code a) -> NS (K ()) (Code a)
    forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
    map_NS (K () a -> NP I a -> K () a
    forall a b. a -> b -> a
    const (() -> K () a
    forall k a (b :: k). a -> K a b
    K ())) (NS (NP I) (Code a) -> NS (K ()) (Code a))
    -> (a -> NS (NP I) (Code a)) -> a -> NS (K ()) (Code a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP I (Code a) -> NS (NP I) (Code a)
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP (SOP I (Code a) -> NS (NP I) (Code a))
    -> (a -> SOP I (Code a)) -> a -> NS (NP I) (Code a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SOP I (Code a)
    forall a. Generic a => a -> Rep a
    from
    {-# INLINE enumTypeFrom #-}

    -- | Convert a sum representation to ihe original type.
    --
    enumTypeTo :: IsEnumType a => NS (K ()) (Code a) -> a
    enumTypeTo :: forall a. IsEnumType a => NS (K ()) (Code a) -> a
    enumTypeTo = Rep a -> a
    forall a. Generic a => Rep a -> a
    to (Rep a -> a)
    -> (NS (K ()) (Code a) -> Rep a) -> NS (K ()) (Code a) -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (NP I) (Code a) -> Rep a
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NS (NP I) (Code a) -> Rep a)
    -> (NS (K ()) (Code a) -> NS (NP I) (Code a))
    -> NS (K ()) (Code a)
    -> Rep a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy ((~) '[])
    -> (forall (a :: [*]). ('[] ~ a) => K () a -> NP I a)
    -> NS (K ()) (Code a)
    -> NS (NP I) (Code a)
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs
    cmap_NS (Proxy ((~) '[])
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy ((~) '[])) (NP I a -> K () a -> NP I a
    forall a b. a -> b -> a
    const NP I a
    NP I '[]
    forall {k} (a :: k -> *). NP a '[]
    Nil)
    {-# INLINE enumTypeTo #-}

    -- | Constraint that captures that a datatype is a single-constructor,
    -- single-field datatype. This always holds for newtype-defined types,
    -- but it can also be true for data-defined types.
    --
    -- The constraint also gives access to the type that is wrapped.
    --
    -- @since 0.3.1.0
    --
    type IsWrappedType (a :: Type) (x :: Type) =
      (Generic a, Code a ~ '[ '[ x ] ])

    -- | Direct access to the part of the code that is relevant
    -- for wrapped types and newtypes.
    --
    -- @since 0.4.0.0
    --
    type WrappedCode (a :: Type) =
      Head (Head (Code a))

    -- | Convert from a wrapped type to its inner type.
    --
    -- @since 0.4.0.0
    --
    wrappedTypeFrom :: IsWrappedType a x => a -> x
    wrappedTypeFrom :: forall a x. IsWrappedType a x => a -> x
    wrappedTypeFrom = I x -> x
    forall a. I a -> a
    unI (I x -> x) -> (a -> I x) -> a -> x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP I '[x] -> I x
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
    hd (NP I '[x] -> I x) -> (a -> NP I '[x]) -> a -> I x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (NP I) '[ '[x]] -> NP I '[x]
    forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
    unZ (NS (NP I) '[ '[x]] -> NP I '[x])
    -> (a -> NS (NP I) '[ '[x]]) -> a -> NP I '[x]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP I '[ '[x]] -> NS (NP I) '[ '[x]]
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP (SOP I '[ '[x]] -> NS (NP I) '[ '[x]])
    -> (a -> SOP I '[ '[x]]) -> a -> NS (NP I) '[ '[x]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SOP I '[ '[x]]
    a -> Rep a
    forall a. Generic a => a -> Rep a
    from
    {-# INLINE wrappedTypeFrom #-}

    -- | Convert a type to a wrapped type.
    --
    -- @since 0.4.0.0
    --
    wrappedTypeTo :: IsWrappedType a x => x -> a
    wrappedTypeTo :: forall a x. IsWrappedType a x => x -> a
    wrappedTypeTo = SOP I '[ '[x]] -> a
    Rep a -> a
    forall a. Generic a => Rep a -> a
    to (SOP I '[ '[x]] -> a) -> (x -> SOP I '[ '[x]]) -> x -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (NP I) '[ '[x]] -> SOP I '[ '[x]]
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NS (NP I) '[ '[x]] -> SOP I '[ '[x]])
    -> (x -> NS (NP I) '[ '[x]]) -> x -> SOP I '[ '[x]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP I '[x] -> NS (NP I) '[ '[x]]
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
    Z (NP I '[x] -> NS (NP I) '[ '[x]])
    -> (x -> NP I '[x]) -> x -> NS (NP I) '[ '[x]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (I x -> NP I '[] -> NP I '[x]
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
    a x -> NP a xs -> NP a (x : xs)
    :* NP I '[]
    forall {k} (a :: k -> *). NP a '[]
    Nil) (I x -> NP I '[x]) -> (x -> I x) -> x -> NP I '[x]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . x -> I x
    forall a. a -> I a
    I
    {-# INLINE wrappedTypeTo #-}

    -- | Constraint that captures that a datatype is a newtype.
    -- This makes use of the fact that newtypes are always coercible
    -- to the type they wrap, whereas datatypes are not.
    --
    -- @since 0.3.1.0
    --
    type IsNewtype (a :: Type) (x :: Type) =
      (IsWrappedType a x, Coercible a x)

    -- | Convert a newtype to its inner type.
    --
    -- This is a specialised synonym for 'coerce'.
    --
    -- @since 0.4.0.0
    --
    newtypeFrom :: IsNewtype a x => a -> x
    newtypeFrom :: forall a x. IsNewtype a x => a -> x
    newtypeFrom = a -> x
    forall a b. Coercible a b => a -> b
    coerce
    {-# INLINE newtypeFrom #-}

    -- | Convert a type to a newtype.
    --
    -- This is a specialised synonym for 'coerce'.
    --
    -- @since 0.4.0.0
    --
    newtypeTo :: IsNewtype a x => x -> a
    newtypeTo :: forall a x. IsNewtype a x => x -> a
    newtypeTo = x -> a
    forall a b. Coercible a b => a -> b
    coerce
    {-# INLINE newtypeTo #-}