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

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

    module Data.Generics.Sum.Internal.Constructors
      ( GAsConstructor (..)
      , GAsConstructor'

      , Context'
      , Context
      , Context_
      , Context0

      , derived0
      ) where

    import Data.Generics.Internal.Families
    import Data.Generics.Internal.Errors
    import Data.Generics.Product.Internal.HList

    import GHC.Generics
    import GHC.TypeLits (Symbol)
    import Data.Kind (Constraint, Type)
    import Data.Generics.Internal.Profunctor.Iso
    import Data.Generics.Internal.Profunctor.Prism

    import GHC.TypeLits (TypeError, ErrorMessage (..))

    derived0 :: forall ctor s t a b. Context0 ctor s t a b => Prism s t a b
    derived0 :: forall (ctor :: Symbol) s t a b.
    Context0 ctor s t a b =>
    Prism s t a b
    derived0 = p i (Rep s (ZonkAny 0)) (Rep t (ZonkAny 0)) -> p i s t
    forall a b x. (Generic a, Generic b) => Iso a b (Rep a x) (Rep b x)
    Iso s t (Rep s (ZonkAny 0)) (Rep t (ZonkAny 0))
    repIso (p i (Rep s (ZonkAny 0)) (Rep t (ZonkAny 0)) -> p i s t)
    -> (p i a b -> p i (Rep s (ZonkAny 0)) (Rep t (ZonkAny 0)))
    -> p i a b
    -> p i s t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (ctor :: Symbol) (s :: * -> *) (t :: * -> *) a b x.
    GAsConstructor ctor s t a b =>
    Prism (s x) (t x) a b
    _GCtor @ctor
    {-# INLINE derived0 #-}

    type Context' ctor s a
      = ( Context0 ctor s s a a
        , ErrorUnless ctor s (HasCtorP ctor (Rep s)))

    class Context (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b
    instance
      ( ErrorUnless ctor s (HasCtorP ctor (Rep s))
      , GAsConstructor' ctor (Rep s) a -- TODO: add a test similar to #62 for prisms
      , GAsConstructor' ctor (Rep (Indexed s)) a'
      , GAsConstructor ctor (Rep s) (Rep t) a b
      , t ~ Infer s a' b
      , GAsConstructor' ctor (Rep (Indexed t)) b'
      , s ~ Infer t b' a
      ) => Context ctor s t a b

    class Context_ (ctor :: Symbol) s t a b
    instance
      ( ErrorUnless ctor s (HasCtorP ctor (Rep s))
      , GAsConstructor' ctor (Rep s) a -- TODO: add a test similar to #62 for prisms
      , GAsConstructor' ctor (Rep (Indexed s)) a'
      , GAsConstructor ctor (Rep s) (Rep t) a b
      , GAsConstructor' ctor (Rep (Indexed t)) b'
      , UnifyHead s t
      , UnifyHead t s
      ) => Context_ ctor s t a b

    type Context0 ctor s t a b
      = ( Generic s
        , Generic t
        , GAsConstructor ctor (Rep s) (Rep t) a b
        , Defined (Rep s)
          (NoGeneric s '[ 'Text "arising from a generic prism focusing on the "
                          ':<>: QuoteType ctor ':<>: 'Text " constructor of type " ':<>: QuoteType a
                        , 'Text "in " ':<>: QuoteType s])
          (() :: Constraint)
        )

    type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
      ErrorUnless ctor s 'False
        = TypeError
            (     'Text "The type "
            ':<>: 'ShowType s
            ':<>: 'Text " does not contain a constructor named "
            ':<>: 'ShowType ctor
            )

      ErrorUnless _ _ 'True
        = ()
    --------------------------------------------------------------------------------

    -- |As 'AsConstructor' but over generic representations as defined by
    --  "GHC.Generics".
    class GAsConstructor (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b where
      _GCtor :: Prism (s x) (t x) a b

    type GAsConstructor' ctor s a = GAsConstructor ctor s s a a

    instance
      ( GIsList f g as bs
      , ListTuple a b as bs
      ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) (M1 C ('MetaCons ctor fixity fields) g) a b where

      _GCtor :: forall x.
    Prism
      (M1 C ('MetaCons ctor fixity fields) f x)
      (M1 C ('MetaCons ctor fixity fields) g x)
      a
      b
    _GCtor = p i (f x) (g x)
    -> p i
         (M1 C ('MetaCons ctor fixity fields) f x)
         (M1 C ('MetaCons ctor fixity fields) g 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) (g x)
     -> p i
          (M1 C ('MetaCons ctor fixity fields) f x)
          (M1 C ('MetaCons ctor fixity fields) g x))
    -> (p i a b -> p i (f x) (g x))
    -> p i a b
    -> p i
         (M1 C ('MetaCons ctor fixity fields) f x)
         (M1 C ('MetaCons ctor fixity fields) g x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i (HList as) (HList bs) -> p i (f x) (g x)
    forall x. Iso (f x) (g x) (HList as) (HList bs)
    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 bs) -> p i (f x) (g x))
    -> (p i a b -> p i (HList as) (HList bs))
    -> p i a b
    -> p i (f x) (g x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . p i a b -> p i (HList as) (HList bs)
    forall tuple tuple' (as :: [*]) (bs :: [*]).
    ListTuple tuple tuple' as bs =>
    Iso (HList as) (HList bs) tuple tuple'
    Iso (HList as) (HList bs) a b
    tupled
      {-# INLINE _GCtor #-}

    instance GSumAsConstructor ctor (HasCtorP ctor l) l r l' r' a b => GAsConstructor ctor (l :+: r) (l' :+: r') a b where
      _GCtor :: forall x. Prism ((:+:) l r x) ((:+:) l' r' x) a b
    _GCtor = forall (ctor :: Symbol) (contains :: Bool) (l :: * -> *)
           (r :: * -> *) (l' :: * -> *) (r' :: * -> *) a b x.
    GSumAsConstructor ctor contains l r l' r' a b =>
    Prism ((:+:) l r x) ((:+:) l' r' x) a b
    _GSumCtor @ctor @(HasCtorP ctor l)
      {-# INLINE _GCtor #-}

    instance GAsConstructor ctor f f' a b => GAsConstructor ctor (M1 D meta f) (M1 D meta f') a b where
      _GCtor :: forall x. Prism (M1 D meta f x) (M1 D meta f' x) a b
    _GCtor = 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 b -> p i (f x) (f' x))
    -> p i a b
    -> p i (M1 D meta f x) (M1 D meta f' x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (ctor :: Symbol) (s :: * -> *) (t :: * -> *) a b x.
    GAsConstructor ctor s t a b =>
    Prism (s x) (t x) a b
    _GCtor @ctor
      {-# INLINE _GCtor #-}

    class GSumAsConstructor (ctor :: Symbol) (contains :: Bool) l r l' r' a b | ctor l r -> a, ctor l' r' -> b where
      _GSumCtor :: Prism ((l :+: r) x) ((l' :+: r') x) a b

    instance GAsConstructor ctor l l' a b => GSumAsConstructor ctor 'True l r l' r a b where
      _GSumCtor :: forall x. Prism ((:+:) l r x) ((:+:) l' r x) a b
    _GSumCtor = 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 b -> p i (l x) (l' x))
    -> p i a b
    -> p i ((:+:) l r x) ((:+:) l' r x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (ctor :: Symbol) (s :: * -> *) (t :: * -> *) a b x.
    GAsConstructor ctor s t a b =>
    Prism (s x) (t x) a b
    _GCtor @ctor
      {-# INLINE _GSumCtor #-}

    instance GAsConstructor ctor r r' a b => GSumAsConstructor ctor 'False l r l r' a b where
      _GSumCtor :: forall x. Prism ((:+:) l r x) ((:+:) l r' x) a b
    _GSumCtor = 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 b -> p i (r x) (r' x))
    -> p i a b
    -> p i ((:+:) l r x) ((:+:) l r' x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (ctor :: Symbol) (s :: * -> *) (t :: * -> *) a b x.
    GAsConstructor ctor s t a b =>
    Prism (s x) (t x) a b
    _GCtor @ctor
      {-# INLINE _GSumCtor #-}