    {-# LANGUAGE DataKinds             #-}
    {-# LANGUAGE PolyKinds             #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE TypeOperators         #-}
    {-# LANGUAGE UndecidableInstances  #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Generics.Internal.Families.Has
    -- Copyright   :  (C) 2020 Csongor Kiss
    -- License     :  BSD3
    -- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -----------------------------------------------------------------------------
    module Data.Generics.Internal.Families.Has
      ( HasTotalFieldP
      , HasTotalTypeP
      , HasTotalPositionP
      , Pos
      , HasPartialTypeP
      , HasCtorP
      , GTypes
      ) where

    import Data.Type.Bool     (type (||))
    import Data.Type.Equality (type (==))
    import GHC.Generics
    import GHC.TypeLits (Symbol, Nat)
    import Data.Kind (Type)

    import Data.Generics.Product.Internal.HList

    -- Note: these could be factored out into a single traversal

    type family Both (m1 :: Maybe a) (m2 :: Maybe a) :: Maybe a where
      Both ('Just a) ('Just a) = 'Just a

    type family Alt (m1 :: Maybe a) (m2 :: Maybe a) :: Maybe a where
      Alt ('Just a) _ = 'Just a
      Alt _ b = b

    type family HasTotalFieldP (field :: Symbol) f :: Maybe Type where
      HasTotalFieldP field (S1 ('MetaSel ('Just field) _ _ _) (Rec0 t))
        = 'Just t
      HasTotalFieldP field (l :*: r)
        = Alt (HasTotalFieldP field l) (HasTotalFieldP field r)
      HasTotalFieldP field (l :+: r)
        = Both (HasTotalFieldP field l) (HasTotalFieldP field r)
      HasTotalFieldP field (S1 _ _)
        = 'Nothing
      HasTotalFieldP field (C1 _ f)
        = HasTotalFieldP field f
      HasTotalFieldP field (D1 _ f)
        = HasTotalFieldP field f
      HasTotalFieldP field (K1 _ _)
        = 'Nothing
      HasTotalFieldP field U1
        = 'Nothing
      HasTotalFieldP field V1
        = 'Nothing

    type family HasTotalTypeP (typ :: Type) f :: Maybe Type where
      HasTotalTypeP typ (S1 _ (K1 _ typ))
        = 'Just typ
      HasTotalTypeP typ (l :*: r)
        = Alt (HasTotalTypeP typ l) (HasTotalTypeP typ r)
      HasTotalTypeP typ (l :+: r)
        = Both (HasTotalTypeP typ l) (HasTotalTypeP typ r)
      HasTotalTypeP typ (S1 _ _)
        = 'Nothing
      HasTotalTypeP typ (C1 _ f)
        = HasTotalTypeP typ f
      HasTotalTypeP typ (D1 _ f)
        = HasTotalTypeP typ f
      HasTotalTypeP typ (K1 _ _)
        = 'Nothing
      HasTotalTypeP typ U1
        = 'Nothing
      HasTotalTypeP typ V1
        = 'Nothing

    data Pos (p :: Nat)

    type family HasTotalPositionP (pos :: Nat) f :: Maybe Type where
      HasTotalPositionP pos (S1 _ (K1 (Pos pos) t))
        = 'Just t
      HasTotalPositionP pos (l :*: r)
        = Alt (HasTotalPositionP pos l) (HasTotalPositionP pos r)
      HasTotalPositionP pos (l :+: r)
        = Both (HasTotalPositionP pos l) (HasTotalPositionP pos r)
      HasTotalPositionP pos (S1 _ _)
        = 'Nothing
      HasTotalPositionP pos (C1 _ f)
        = HasTotalPositionP pos f
      HasTotalPositionP pos (D1 _ f)
        = HasTotalPositionP pos f
      HasTotalPositionP pos (K1 _ _)
        = 'Nothing
      HasTotalPositionP pos U1
        = 'Nothing
      HasTotalPositionP pos V1
        = 'Nothing

    type family HasPartialTypeP a f :: Bool where
      HasPartialTypeP t (l :+: r)
        = HasPartialTypeP t l || HasPartialTypeP t r
      HasPartialTypeP t (C1 m f)
        = t == GTypes f
      HasPartialTypeP t (M1 _ _ f)
        = HasPartialTypeP t f
      HasPartialTypeP t _
        = 'False

    type family HasCtorP (ctor :: Symbol) f :: Bool where
      HasCtorP ctor (C1 ('MetaCons ctor _ _) _)
        = 'True
      HasCtorP ctor (f :+: g)
        = HasCtorP ctor f || HasCtorP ctor g
      HasCtorP ctor (D1 m f)
        = HasCtorP ctor f
      HasCtorP ctor _
        = 'False

    type family GTypes (rep :: Type -> Type) :: [Type] where
      GTypes (l :*: r)
        = GTypes l ++ GTypes r
      GTypes (K1 _ a)
        = '[ a]
      GTypes (M1 _ m a)
        = GTypes a
      GTypes U1 = '[]