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

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Generics.Product.Internal.GLens
    -- Copyright   :  (C) 2020 Csongor Kiss
    -- License     :  BSD3
    -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Derive record field getters and setters generically.
    --
    -----------------------------------------------------------------------------

    module Data.Generics.Product.Internal.GLens
      ( GLens (..)
      , GLens'
      , TyFun
      , Eval
      ) where

    import Data.Generics.Internal.Profunctor.Lens (Lens, choosing, first, second)
    import Data.Generics.Internal.Profunctor.Iso (kIso, sumIso, mIso)

    import Data.Kind    (Type)
    import GHC.Generics

    type Pred = TyFun (Type -> Type) (Maybe Type)

    type TyFun a b = a -> b -> Type
    type family Eval (f :: TyFun a b) (x :: a) :: b

    -- A generic lens that uses some predicate to determine which field to focus on
    class GLens (pred :: Pred) (s :: Type -> Type) (t :: Type -> Type) a b | s pred -> a, t pred -> b where
      glens :: Lens (s x) (t x) a b

    type GLens' pred s a = GLens pred s s a a

    instance GProductLens (Eval pred l) pred l r l' r' a b
          => GLens pred (l :*: r) (l' :*: r') a b where

      glens :: forall x. Lens ((:*:) l r x) ((:*:) l' r' x) a b
    glens = forall (left :: Maybe (*)) (pred :: Pred) (l :: * -> *)
           (r :: * -> *) (l' :: * -> *) (r' :: * -> *) a b x.
    GProductLens left pred l r l' r' a b =>
    Lens ((:*:) l r x) ((:*:) l' r' x) a b
    forall {k} (left :: Maybe (*)) (pred :: Pred) (l :: k -> *)
           (r :: k -> *) (l' :: k -> *) (r' :: k -> *) a b (x :: k).
    GProductLens left pred l r l' r' a b =>
    Lens ((:*:) l r x) ((:*:) l' r' x) a b
    gproductLens @(Eval pred l) @pred
      {-# INLINE glens #-}

    instance (GLens pred l l' a b, GLens pred r r' a b) =>  GLens pred (l :+: r) (l' :+: r') a b where
      glens :: forall x. Lens ((:+:) l r x) ((:+:) l' r' x) a b
    glens = p i (Either (l x) (r x)) (Either (l' x) (r' x))
    -> p i ((:+:) l r x) ((:+:) l' r' x)
    forall (a :: * -> *) (b :: * -> *) x (a' :: * -> *) (b' :: * -> *)
           (p :: * -> * -> * -> *) i.
    Profunctor p =>
    p i (Either (a x) (b x)) (Either (a' x) (b' x))
    -> p i ((:+:) a b x) ((:+:) a' b' x)
    sumIso (p i (Either (l x) (r x)) (Either (l' x) (r' x))
     -> p i ((:+:) l r x) ((:+:) l' r' x))
    -> (p i a b -> p i (Either (l x) (r x)) (Either (l' 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
    . Lens (l x) (l' x) a b
    -> Lens (r x) (r' x) a b
    -> Lens (Either (l x) (r x)) (Either (l' x) (r' x)) a b
    forall s t a b s' t'.
    Lens s t a b
    -> Lens s' t' a b -> Lens (Either s s') (Either t t') a b
    choosing (forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @pred) (forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @pred)
      {-# INLINE glens #-}

    instance GLens pred (K1 r a) (K1 r b) a b where
      glens :: forall x. Lens (K1 r a x) (K1 r b x) a b
    glens = p i a b -> p i (K1 r a x) (K1 r b x)
    forall r a p1 b (p2 :: * -> * -> * -> *) i.
    Profunctor p2 =>
    p2 i a b -> p2 i (K1 r a p1) (K1 r b p1)
    kIso
      {-# INLINE glens #-}

    instance (GLens pred f g a b) => GLens pred (M1 m meta f) (M1 m meta g) a b where
      glens :: forall x. Lens (M1 m meta f x) (M1 m meta g x) a b
    glens = p i (f x) (g x) -> p i (M1 m meta f x) (M1 m meta 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 m meta f x) (M1 m meta g x))
    -> (p i a b -> p i (f x) (g x))
    -> p i a b
    -> p i (M1 m meta f x) (M1 m meta g x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @pred
      {-# INLINE glens #-}

    class GProductLens (left :: Maybe Type) (pred :: Pred) l r l' r' a b | pred l r -> a, pred l' r' -> b where
      gproductLens :: Lens ((l :*: r) x) ((l' :*: r') x) a b

    instance GLens pred l l' a b => GProductLens ('Just x) pred l r l' r a b where
      gproductLens :: forall x. Lens ((:*:) l r x) ((:*:) l' r x) a b
    gproductLens = p i (l x) (l' x) -> p i ((:*:) l r x) ((:*:) l' r x)
    forall (a :: * -> *) (b :: * -> *) x (a' :: * -> *)
           (p :: * -> * -> * -> *) i.
    Strong p =>
    p i (a x) (a' x) -> p i ((:*:) a b x) ((:*:) a' b x)
    first (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 (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @pred
      {-# INLINE gproductLens #-}

    instance GLens pred r r' a b => GProductLens 'Nothing pred l r l r' a b where
      gproductLens :: forall x. Lens ((:*:) l r x) ((:*:) l r' x) a b
    gproductLens = p i (r x) (r' x) -> p i ((:*:) l r x) ((:*:) l r' x)
    forall (a :: * -> *) (b :: * -> *) x (b' :: * -> *)
           (p :: * -> * -> * -> *) i.
    Strong p =>
    p i (b x) (b' x) -> p i ((:*:) a b x) ((:*:) a b' x)
    second (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 (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @pred
      {-# INLINE gproductLens #-}