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

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Generics.Product.Internal.Subtype
    -- Copyright   :  (C) 2020 Csongor Kiss
    -- License     :  BSD3
    -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Structural subtype relationships between product types.
    --
    -----------------------------------------------------------------------------

    module Data.Generics.Product.Internal.Subtype
      ( Context
      , GSmash (..)
      , GUpcast (..)
      ) where

    import Data.Generics.Internal.Families
    import Data.Generics.Product.Internal.GLens

    import Data.Kind (Type)
    import GHC.Generics
    import GHC.TypeLits (Symbol)
    import Data.Generics.Internal.Profunctor.Lens (view)

    import GHC.TypeLits (TypeError, ErrorMessage (..))
    import Data.Kind (Constraint)
    import Data.Generics.Internal.Errors

    type Context a b
      = ( Generic a
        , Generic b
        , GSmash (Rep a) (Rep b)
        , GUpcast (Rep a) (Rep b)
        , CustomError a b
        )

    type family CustomError a b :: Constraint where
      CustomError a b =
        ( ErrorUnless b a (CollectFieldsOrdered (Rep b) \\ CollectFieldsOrdered (Rep a))
        , Defined (Rep a)
          (NoGeneric a '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b
                        , 'Text "as a supertype of " ':<>: QuoteType a
                        ])
          (() :: Constraint)
        , Defined (Rep b)
          (NoGeneric b '[ 'Text "arising from a generic lens focusing on " ':<>: QuoteType b
                        , 'Text "as a supertype of " ':<>: QuoteType a
                        ])
          (() :: Constraint)
        )

    type family ErrorUnless (sup :: Type) (sub :: Type) (diff :: [Symbol]) :: Constraint where
      ErrorUnless _ _ '[]
        = ()

      ErrorUnless sup sub fs
        = TypeError
            (     'Text "The type '"
            ':<>: 'ShowType sub
            ':<>: 'Text "' is not a subtype of '"
            ':<>: 'ShowType sup ':<>: 'Text "'."
            ':$$: 'Text "The following fields are missing from '"
            ':<>: 'ShowType sub ':<>: 'Text "':"
            ':$$: ShowSymbols fs
            )

    --------------------------------------------------------------------------------
    -- * Generic upcasting

    class GUpcast (sub :: Type -> Type) (sup :: Type -> Type) where
      gupcast :: sub p -> sup p

    instance (GUpcast sub a, GUpcast sub b) => GUpcast sub (a :*: b) where
      gupcast :: forall p. sub p -> (:*:) a b p
    gupcast sub p
    rep = sub p -> a p
    forall p. sub p -> a p
    forall (sub :: * -> *) (sup :: * -> *) p.
    GUpcast sub sup =>
    sub p -> sup p
    gupcast sub p
    rep a p -> b p -> (:*:) a b p
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: sub p -> b p
    forall p. sub p -> b p
    forall (sub :: * -> *) (sup :: * -> *) p.
    GUpcast sub sup =>
    sub p -> sup p
    gupcast sub p
    rep

    instance
      GLens' (HasTotalFieldPSym field) sub t
      => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where

      gupcast :: forall p. sub p -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    gupcast sub p
    r = Rec0 t p -> M1 S ('MetaSel ('Just field) p f b) (Rec0 t) p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (t -> Rec0 t p
    forall k i c (p :: k). c -> K1 i c p
    K1 (Lens (sub p) (sub p) t t -> sub p -> t
    forall s a. Lens s s a a -> s -> a
    view (forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @(HasTotalFieldPSym field)) sub p
    r))

    instance GUpcast sub sup => GUpcast sub (C1 c sup) where
      gupcast :: forall p. sub p -> C1 c sup p
    gupcast = sup p -> M1 C c sup p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (sup p -> M1 C c sup p)
    -> (sub p -> sup p) -> sub p -> M1 C c sup p
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sub p -> sup p
    forall p. sub p -> sup p
    forall (sub :: * -> *) (sup :: * -> *) p.
    GUpcast sub sup =>
    sub p -> sup p
    gupcast

    instance GUpcast sub sup => GUpcast sub (D1 c sup) where
      gupcast :: forall p. sub p -> D1 c sup p
    gupcast = sup p -> M1 D c sup p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (sup p -> M1 D c sup p)
    -> (sub p -> sup p) -> sub p -> M1 D c sup p
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sub p -> sup p
    forall p. sub p -> sup p
    forall (sub :: * -> *) (sup :: * -> *) p.
    GUpcast sub sup =>
    sub p -> sup p
    gupcast

    --------------------------------------------------------------------------------
    -- * Generic smashing

    class GSmash sub sup where
      gsmash :: sup p -> sub p -> sub p

    instance (GSmash a sup, GSmash b sup) => GSmash (a :*: b) sup where
      gsmash :: forall (p :: k). sup p -> (:*:) a b p -> (:*:) a b p
    gsmash sup p
    rep (a p
    a :*: b p
    b) = sup p -> a p -> a p
    forall (p :: k). sup p -> a p -> a p
    forall {k} (sub :: k -> *) (sup :: k -> *) (p :: k).
    GSmash sub sup =>
    sup p -> sub p -> sub p
    gsmash sup p
    rep a p
    a a p -> b p -> (:*:) a b p
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: sup p -> b p -> b p
    forall (p :: k). sup p -> b p -> b p
    forall {k} (sub :: k -> *) (sup :: k -> *) (p :: k).
    GSmash sub sup =>
    sup p -> sub p -> sub p
    gsmash sup p
    rep b p
    b

    instance
      ( leaf ~ (S1 ('MetaSel ('Just field) p f b) t)
      , GSmashLeaf leaf sup (HasTotalFieldP field sup)
      ) => GSmash (S1 ('MetaSel ('Just field) p f b) t) sup where

      gsmash :: forall (p :: k).
    sup p
    -> S1 ('MetaSel ('Just field) p f b) t p
    -> S1 ('MetaSel ('Just field) p f b) t p
    gsmash = forall {k} (sub :: k -> *) (sup :: k -> *) (w :: Maybe (*))
           (p :: k).
    GSmashLeaf sub sup w =>
    sup p -> sub p -> sub p
    forall (sub :: k -> *) (sup :: k -> *) (w :: Maybe (*)) (p :: k).
    GSmashLeaf sub sup w =>
    sup p -> sub p -> sub p
    gsmashLeaf @_ @_ @(HasTotalFieldP field sup)

    instance GSmash sub sup => GSmash (C1 c sub) sup where
      gsmash :: forall (p :: k). sup p -> C1 c sub p -> C1 c sub p
    gsmash sup p
    sup (M1 sub p
    sub) = sub p -> M1 C c sub p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (sup p -> sub p -> sub p
    forall (p :: k). sup p -> sub p -> sub p
    forall {k} (sub :: k -> *) (sup :: k -> *) (p :: k).
    GSmash sub sup =>
    sup p -> sub p -> sub p
    gsmash sup p
    sup sub p
    sub)

    instance GSmash sub sup => GSmash (D1 c sub) sup where
      gsmash :: forall (p :: k). sup p -> D1 c sub p -> D1 c sub p
    gsmash sup p
    sup (M1 sub p
    sub) = sub p -> M1 D c sub p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (sup p -> sub p -> sub p
    forall (p :: k). sup p -> sub p -> sub p
    forall {k} (sub :: k -> *) (sup :: k -> *) (p :: k).
    GSmash sub sup =>
    sup p -> sub p -> sub p
    gsmash sup p
    sup sub p
    sub)

    class GSmashLeaf sub sup (w :: Maybe Type) where
      gsmashLeaf :: sup p -> sub p -> sub p

    instance
      GLens' (HasTotalFieldPSym field) sup t
      => GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup ('Just t) where
      gsmashLeaf :: forall p.
    sup p
    -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    gsmashLeaf sup p
    sup S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    _ = Rec0 t p -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (t -> Rec0 t p
    forall k i c (p :: k). c -> K1 i c p
    K1 (Lens (sup p) (sup p) t t -> sup p -> t
    forall s a. Lens s s a a -> s -> a
    view (forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
    GLens pred s t a b =>
    Lens (s x) (t x) a b
    glens @(HasTotalFieldPSym field)) sup p
    sup))

    instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'Nothing where
      gsmashLeaf :: forall (p :: k).
    sup p
    -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    gsmashLeaf sup p
    _ = S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    -> S1 ('MetaSel ('Just field) p f b) (Rec0 t) p
    forall a. a -> a
    id

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