content: {-# 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 = '[]
  
  