    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_HADDOCK not-home #-}

    -- | This module is intended for internal use only, and may change without
    -- warning in subsequent releases.
    module Optics.Internal.Generic.TypeLevel
      ( -- * Pathing
        PathTree(..)
      , Path(..)
      -- ** Names
      , GetFieldPaths
      , GetNamePath
      -- ** Positions
      , GetPositionPaths
      , GetPositionPath
      -- * Misc
      , HideReps
      , AnyHasPath
      , NoGenericError
      ) where

    import Data.Kind
    import Data.Type.Bool
    import Data.Type.Equality
    import GHC.Generics
    import GHC.TypeLits

    import Optics.Internal.Optic.TypeLevel

    -- | A map that allows reaching a specific field in a generic representation of
    -- a data type. Computed up front by generic optics for early error reporting
    -- and efficient data traversal.
    data PathTree e
      = PathTree (PathTree e) (PathTree e)
      | PathLeaf (Either e [Path])

    data Path = PathLeft | PathRight

    ----------------------------------------
    -- Paths to a field

    -- | Compute paths to a field with a specific name.
    type family GetFieldPaths s (name :: Symbol) g :: PathTree Symbol where
      GetFieldPaths s name (M1 D _ g)  = GetFieldPaths s name g
      GetFieldPaths s name (g1 :+: g2) = 'PathTree (GetFieldPaths s name g1)
                                                   (GetFieldPaths s name g2)
      GetFieldPaths s name (M1 C _ g)  = 'PathLeaf (GetNamePath name g '[])

      GetFieldPaths s name V1 = TypeError ('Text "Type " ':<>: QuoteType s ':<>:
                                           'Text " has no data constructors")

    -- | Compute path to a constructor in a sum or a field in a product with a
    -- specific name.
    type family GetNamePath (name :: Symbol) g (acc :: [Path]) :: Either Symbol [Path] where
      GetNamePath name (M1 D _ g) acc = GetNamePath name g acc

      -- Find path to a constructor in a sum type.
      GetNamePath name (M1 C ('MetaCons name _ _) _) acc = 'Right (Reverse acc '[])
      GetNamePath name (g1 :+: g2) acc = FirstRight (GetNamePath name g1 ('PathLeft  : acc))
                                                    (GetNamePath name g2 ('PathRight : acc))

      -- Find path to a field in a product type.
      GetNamePath name (M1 S ('MetaSel ('Just name) _ _ _) _) acc = 'Right (Reverse acc '[])
      GetNamePath name (g1 :*: g2) acc = FirstRight (GetNamePath name g1 ('PathLeft  : acc))
                                                    (GetNamePath name g2 ('PathRight : acc))

      GetNamePath name _ _ = 'Left name

    ----------------------------------------
    -- Paths to a position

    -- | Compute paths to a field at a specific position.
    type family GetPositionPaths s (pos :: Nat) g :: PathTree (Nat, Nat) where
      GetPositionPaths s pos (M1 D _ g)  = GetPositionPaths s pos g
      GetPositionPaths s pos (g1 :+: g2) = 'PathTree (GetPositionPaths s pos g1)
                                                     (GetPositionPaths s pos g2)
      GetPositionPaths s pos (M1 C _ g)  = 'PathLeaf (GetPositionPath pos g 0 '[])

      GetPositionPaths s pos V1 = TypeError ('Text "Type " ':<>: QuoteType s ':<>:
                                             'Text " has no data constructors")

    -- | Compute path to a constructor in a sum or a field in a product at a
    -- specific position.
    type family GetPositionPath (pos :: Nat) g (k :: Nat) (acc :: [Path])
      :: Either (Nat, Nat) [Path] where
      GetPositionPath pos (M1 D _ g) k acc = GetPositionPath pos g k acc

      -- Find field at a position in a sum type.
      GetPositionPath pos (M1 C _ _) k acc =
        If (pos == k + 1) ('Right (Reverse acc '[])) ('Left '(pos, k + 1))
      GetPositionPath pos (g1 :+: g2) k acc =
        ContinueWhenLeft (GetPositionPath pos g1 k ('PathLeft : acc)) g2 acc

      -- Find field at a position in a product type.
      GetPositionPath pos (M1 S _ _) k acc =
        If (pos == k + 1) ('Right (Reverse acc '[])) ('Left '(pos, k + 1))
      GetPositionPath pos (g1 :*: g2) k acc =
        ContinueWhenLeft (GetPositionPath pos g1 k ('PathLeft : acc)) g2 acc

      -- The second element is the number of fields in the data constructor.
      GetPositionPath pos _ k _ = 'Left '(pos, k)

    -- | If the left branch had the position we're looking for, return it. Otherwise
    -- continue with the right branch.
    type family ContinueWhenLeft (r :: Either (Nat, Nat) [Path]) g acc
      :: Either (Nat, Nat) [Path] where
      ContinueWhenLeft ('Right path) _ _ = 'Right path
      ContinueWhenLeft ('Left '(pos, k)) g acc = GetPositionPath pos g k ('PathRight : acc)

    ----------------------------------------
    -- Misc

    data Void1 a
    -- | Generate bogus equality constraints that attempt to unify generic
    -- representations with this type in case there is an error such as missing
    -- field, constructor etc. so these huge types don't leak into error messages.
    type family HideReps (g :: Type -> Type) (h :: Type -> Type) :: Constraint where
      HideReps g h = (g ~ Void1, h ~ Void1)

    -- | Check if any leaf in the tree has a '[Path]'.
    type family AnyHasPath (path :: PathTree e) :: Bool where
      AnyHasPath ('PathTree path1 path2) = AnyHasPath path1 || AnyHasPath path2
      AnyHasPath ('PathLeaf ('Right _))  = 'True
      AnyHasPath ('PathLeaf ('Left _ ))  = 'False

    type family NoGenericError t where
      NoGenericError t = TypeError
        ('Text "Type " ':<>: QuoteType t ':<>:
         'Text " doesn't have a Generic instance")