    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE AllowAmbiguousTypes   #-}
    {-# LANGUAGE DataKinds             #-}
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE KindSignatures        #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeApplications      #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE UndecidableInstances  #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Generics.Sum.Internal.Typed
    -- Copyright   :  (C) 2020 Csongor Kiss
    -- License     :  BSD3
    -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Derive constructor-field-type-based prisms generically.
    --
    -----------------------------------------------------------------------------

    module Data.Generics.Sum.Internal.Typed
      ( Context
      , derived
      , GAsType (..)
      ) where

    import Data.Kind
    import GHC.Generics

    import GHC.TypeLits (TypeError, ErrorMessage (..), Symbol)
    import Data.Generics.Internal.Errors
    import Data.Generics.Internal.Families
    import Data.Generics.Product.Internal.HList
    import Data.Generics.Internal.Profunctor.Iso
    import Data.Generics.Internal.Profunctor.Prism

    type Context a s
      = ( Generic s
        , ErrorUnlessOne a s (CollectPartialType (TupleToList a) (Rep s))
        , GAsType (Rep s) a
        , Defined (Rep s)
          (NoGeneric s '[ 'Text "arising from a generic prism focusing on a constructor of type " ':<>: QuoteType a])
          (() :: Constraint)
        )

    derived :: Context a s => Prism' s a
    derived :: forall a s. Context a s => Prism' s a
    derived = p i (Rep s (ZonkAny 0)) (Rep s (ZonkAny 0)) -> p i s s
    forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
    Iso s s (Rep s (ZonkAny 0)) (Rep s (ZonkAny 0))
    repIso (p i (Rep s (ZonkAny 0)) (Rep s (ZonkAny 0)) -> p i s s)
    -> (p i a a -> p i (Rep s (ZonkAny 0)) (Rep s (ZonkAny 0)))
    -> p i a a
    -> p i s s
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a a -> p i (Rep s (ZonkAny 0)) (Rep s (ZonkAny 0))
    forall x. Prism (Rep s x) (Rep s x) a a
    forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
    _GTyped
    {-# INLINE derived #-}

    type family ErrorUnlessOne (a :: Type) (s :: Type) (ctors :: [Symbol]) :: Constraint where
      ErrorUnlessOne _ _ '[_]
        = ()

      ErrorUnlessOne a s '[]
        = TypeError
            (     'Text "The type "
            ':<>: 'ShowType s
            ':<>: 'Text " does not contain a constructor whose field is of type "
            ':<>: 'ShowType a
            )

      ErrorUnlessOne a s cs
        = TypeError
            (     'Text "The type "
            ':<>: 'ShowType s
            ':<>: 'Text " contains multiple constructors whose fields are of type "
            ':<>: 'ShowType a ':<>: 'Text "."
            ':$$: 'Text "The choice of constructor is thus ambiguous, could be any of:"
            ':$$: ShowSymbols cs
            )

    --------------------------------------------------------------------------------

    -- |As 'AsType' but over generic representations as defined by "GHC.Generics".
    class GAsType (f :: Type -> Type) (as :: Type) where
      _GTyped :: Prism (f x) (f x) as as

    instance
      ( GIsList f f as as
      , ListTuple a a as as
      ) => GAsType (M1 C meta f) a where
      _GTyped :: forall x. Prism (M1 C meta f x) (M1 C meta f x) a a
    _GTyped = p i (f x) (f x) -> p i (M1 C meta f x) (M1 C meta f x)
    forall i1 (c :: Meta) (f :: * -> *) p1 (g :: * -> *)
           (p2 :: * -> * -> * -> *) i2.
    Profunctor p2 =>
    p2 i2 (f p1) (g p1) -> p2 i2 (M1 i1 c f p1) (M1 i1 c g p1)
    mIso (p i (f x) (f x) -> p i (M1 C meta f x) (M1 C meta f x))
    -> (p i a a -> p i (f x) (f x))
    -> p i a a
    -> p i (M1 C meta f x) (M1 C meta f x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList as) (HList as) -> p i (f x) (f x)
    forall x. Iso (f x) (f x) (HList as) (HList as)
    forall (f :: * -> *) (g :: * -> *) (as :: [*]) (bs :: [*]) x.
    GIsList f g as bs =>
    Iso (f x) (g x) (HList as) (HList bs)
    glist (p i (HList as) (HList as) -> p i (f x) (f x))
    -> (p i a a -> p i (HList as) (HList as))
    -> p i a a
    -> p i (f x) (f x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a a -> p i (HList as) (HList as)
    forall tuple tuple' (as :: [*]) (bs :: [*]).
    ListTuple tuple tuple' as bs =>
    Iso (HList as) (HList bs) tuple tuple'
    Iso (HList as) (HList as) a a
    tupled
      {-# INLINE _GTyped #-}

    instance GSumAsType (HasPartialTypeP (TupleToList a) l) l r a => GAsType (l :+: r) a where
      _GTyped :: forall x. Prism ((:+:) l r x) ((:+:) l r x) a a
    _GTyped = forall (contains :: Bool) (l :: * -> *) (r :: * -> *) a x.
    GSumAsType contains l r a =>
    Prism ((:+:) l r x) ((:+:) l r x) a a
    _GSumTyped @(HasPartialTypeP (TupleToList a) l)
      {-# INLINE _GTyped #-}

    instance GAsType f a => GAsType (M1 D meta f) a where
      _GTyped :: forall x. Prism (M1 D meta f x) (M1 D meta f x) a a
    _GTyped = p i (f x) (f x) -> p i (M1 D meta f x) (M1 D meta f x)
    forall i1 (c :: Meta) (f :: * -> *) p1 (g :: * -> *)
           (p2 :: * -> * -> * -> *) i2.
    Profunctor p2 =>
    p2 i2 (f p1) (g p1) -> p2 i2 (M1 i1 c f p1) (M1 i1 c g p1)
    mIso (p i (f x) (f x) -> p i (M1 D meta f x) (M1 D meta f x))
    -> (p i a a -> p i (f x) (f x))
    -> p i a a
    -> p i (M1 D meta f x) (M1 D meta f x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a a -> p i (f x) (f x)
    forall x. Prism (f x) (f x) a a
    forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
    _GTyped
      {-# INLINE _GTyped #-}

    class GSumAsType (contains :: Bool) l r (a :: Type) where
      _GSumTyped :: Prism ((l :+: r) x) ((l :+: r) x) a a

    instance GAsType l a => GSumAsType 'True l r a where
      _GSumTyped :: forall x. Prism ((:+:) l r x) ((:+:) l r x) a a
    _GSumTyped = p i (l x) (l x) -> p i ((:+:) l r x) ((:+:) l r x)
    forall (a :: * -> *) (c :: * -> *) x (b :: * -> *)
           (p :: * -> * -> * -> *) i.
    Choice p =>
    p i (a x) (b x) -> p i ((:+:) a c x) ((:+:) b c x)
    left (p i (l x) (l x) -> p i ((:+:) l r x) ((:+:) l r x))
    -> (p i a a -> p i (l x) (l x))
    -> p i a a
    -> p i ((:+:) l r x) ((:+:) l r x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a a -> p i (l x) (l x)
    forall x. Prism (l x) (l x) a a
    forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
    _GTyped
      {-# INLINE _GSumTyped #-}

    instance GAsType r a => GSumAsType 'False l r a where
      _GSumTyped :: forall x. Prism ((:+:) l r x) ((:+:) l r x) a a
    _GSumTyped = p i (r x) (r x) -> p i ((:+:) l r x) ((:+:) l r x)
    forall (a :: * -> *) (b :: * -> *) x (c :: * -> *)
           (p :: * -> * -> * -> *) i.
    Choice p =>
    p i (b x) (c x) -> p i ((:+:) a b x) ((:+:) a c x)
    right (p i (r x) (r x) -> p i ((:+:) l r x) ((:+:) l r x))
    -> (p i a a -> p i (r x) (r x))
    -> p i a a
    -> p i ((:+:) l r x) ((:+:) l r x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a a -> p i (r x) (r x)
    forall x. Prism (r x) (r x) a a
    forall (f :: * -> *) as x. GAsType f as => Prism (f x) (f x) as as
    _GTyped
      {-# INLINE _GSumTyped #-}