content: {-# 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 rep = gupcast rep :*: gupcast rep
  
  instance
    GLens' (HasTotalFieldPSym field) sub t
    => GUpcast sub (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) where
  
    gupcast r = M1 (K1 (view (glens @(HasTotalFieldPSym field)) r))
  
  instance GUpcast sub sup => GUpcast sub (C1 c sup) where
    gupcast = M1 . gupcast
  
  instance GUpcast sub sup => GUpcast sub (D1 c sup) where
    gupcast = M1 . 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 rep (a :*: b) = gsmash rep a :*: gsmash rep 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 = gsmashLeaf @_ @_ @(HasTotalFieldP field sup)
  
  instance GSmash sub sup => GSmash (C1 c sub) sup where
    gsmash sup (M1 sub) = M1 (gsmash sup sub)
  
  instance GSmash sub sup => GSmash (D1 c sub) sup where
    gsmash sup (M1 sub) = M1 (gsmash sup 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 sup _ = M1 (K1 (view (glens @(HasTotalFieldPSym field)) sup))
  
  instance GSmashLeaf (S1 ('MetaSel ('Just field) p f b) (Rec0 t)) sup 'Nothing where
    gsmashLeaf _ = id
  
  data HasTotalFieldPSym :: Symbol -> (TyFun (Type -> Type) (Maybe Type))
  type instance Eval (HasTotalFieldPSym sym) tt = HasTotalFieldP sym tt
  