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

    module Data.Generics.Product.Internal.Fields
      ( Context_
      , Context'
      , Context0
      , Context
      , derived
      ) where

    import Data.Generics.Internal.Families
    import Data.Generics.Product.Internal.GLens
    import Data.Kind    (Constraint, Type)
    import GHC.Generics
    import GHC.TypeLits (Symbol, ErrorMessage(..), TypeError)
    import Data.Generics.Internal.Errors
    import Data.Generics.Internal.Profunctor.Lens
    import Data.Generics.Internal.Profunctor.Iso

    -- Full context
    class Context (field :: Symbol) s t a b | s field -> a, t field -> b, s field b -> t, t field a -> s
    instance
      ( HasTotalFieldP field (Rep s) ~ 'Just a
      , HasTotalFieldP field (Rep t) ~ 'Just b
      , HasTotalFieldP field (Rep (Indexed s)) ~ 'Just a'
      , HasTotalFieldP field (Rep (Indexed t)) ~ 'Just b'
      , t ~ Infer s a' b
      , s ~ Infer t b' a
      ) => Context field s t a b

    -- Alternative type inference
    type Context_ field s t a b
      = ( HasTotalFieldP field (Rep s) ~ 'Just a
        , HasTotalFieldP field (Rep t) ~ 'Just b
        , UnifyHead s t
        , UnifyHead t s
        )

    -- Monomorphic
    type Context' field s a
      = ( Generic s
        , ErrorUnless field s (CollectField field (Rep s))
        , GLens' (HasTotalFieldPSym field) (Rep s) a
        , Defined (Rep s)
          (NoGeneric s '[ 'Text "arising from a generic lens focusing on the "
                          ':<>: QuoteType field ':<>: 'Text " field of type " ':<>: QuoteType a
                        , 'Text "in " ':<>: QuoteType s])
          (() :: Constraint)
        )

    -- No inference
    type Context0 field s t a b
      = ( Generic s
        , Generic t
        , GLens  (HasTotalFieldPSym field) (Rep s) (Rep t) a b
        , ErrorUnless field s (CollectField field (Rep s))
        , Defined (Rep s)
          (NoGeneric s '[ 'Text "arising from a generic lens focusing on the "
                          ':<>: QuoteType field ':<>: 'Text " field of type " ':<>: QuoteType a
                        , 'Text "in " ':<>: QuoteType s])
          (() :: Constraint)
        )

    derived :: forall field s t a b. Context0 field s t a b => Lens s t a b
    derived :: forall (field :: Symbol) s t a b.
    Context0 field s t a b =>
    Lens s t a b
    derived = 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 (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @(HasTotalFieldPSym field)
    {-# INLINE derived #-}

    type family ErrorUnless (field :: Symbol) (s :: Type) (stat :: TypeStat) :: Constraint where
      ErrorUnless field s ('TypeStat _ _ '[])
        = TypeError
            (     'Text "The type "
            ':<>: 'ShowType s
            ':<>: 'Text " does not contain a field named '"
            ':<>: 'Text field ':<>: 'Text "'."
            )

      ErrorUnless field s ('TypeStat (n ': ns) _ _)
        = TypeError
            (     'Text "Not all constructors of the type "
            ':<>: 'ShowType s
            ':$$: 'Text " contain a field named '"
            ':<>: 'Text field ':<>: 'Text "'."
            ':$$: 'Text "The offending constructors are:"
            ':$$: ShowSymbols (n ': ns)
            )

      ErrorUnless _ _ ('TypeStat '[] '[] _)
        = ()

    data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) (Maybe Type))
    type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt