    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE TypeInType #-}
    {-# 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.Optic.TypeLevel where

    import Data.Kind
    import GHC.TypeLits

    -- | A list of index types, used for indexed optics.
    --
    -- @since 0.2
    type IxList = [Type]

    -- | An alias for an empty index-list
    type NoIx = ('[] :: IxList)

    -- | Singleton index list
    type WithIx i = ('[i] :: IxList)

    ----------------------------------------
    -- Elimination forms in error messages

    type family ShowSymbolWithOrigin symbol origin :: ErrorMessage where
      ShowSymbolWithOrigin symbol origin = 'Text "  "
                                     ':<>: QuoteSymbol symbol
                                     ':<>: 'Text " (from "
                                     ':<>: 'Text origin
                                     ':<>: 'Text ")"

    type family ShowSymbolsWithOrigin (fs :: [(Symbol, Symbol)]) :: ErrorMessage where
      ShowSymbolsWithOrigin '[ '(symbol, origin) ] =
        ShowSymbolWithOrigin symbol origin
      ShowSymbolsWithOrigin ('(symbol, origin) ': rest) =
        ShowSymbolWithOrigin symbol origin ':$$: ShowSymbolsWithOrigin rest

    type family ShowOperators (ops :: [Symbol]) :: ErrorMessage where
      ShowOperators '[op] =
        QuoteSymbol op ':<>: 'Text " (from Optics.Operators)"
      ShowOperators (op ': rest) =
        QuoteSymbol op ':<>: 'Text " " ':<>: ShowOperators rest

    type family AppendEliminations a b where
      AppendEliminations '(fs1, ops1) '(fs2, ops2) =
        '(Append fs1 fs2, Append ops1 ops2)

    type family ShowEliminations forms :: ErrorMessage where
      ShowEliminations '(fs, ops) =
        ShowSymbolsWithOrigin fs ':$$: 'Text "  " ':<>: ShowOperators ops

    ----------------------------------------
    -- Lists

    -- | Reverse a type-level list.
    type family Reverse (xs :: [k]) (acc :: [k]) :: [k] where
      Reverse '[]      acc = acc
      Reverse (x : xs) acc = Reverse xs (x : acc)

    -- | Curry a type-level list.
    --
    -- In pseudo (dependent-)Haskell:
    --
    -- @
    -- 'Curry' xs y = 'foldr' (->) y xs
    -- @
    type family Curry (xs :: IxList) (y :: Type) :: Type where
      Curry '[]       y = y
      Curry (x ': xs) y = x -> Curry xs y

    -- | Append two type-level lists together.
    type family Append (xs :: [k]) (ys :: [k]) :: [k] where
      Append '[]       ys  = ys -- needed for (<%>) and (%>)
      Append xs        '[] = xs -- needed for (<%)
      Append (x ': xs) ys  = x ': Append xs ys

    -- | Class that is inhabited by all type-level lists @xs@, providing the ability
    -- to compose a function under @'Curry' xs@.
    class CurryCompose xs where
      -- | Compose a function under @'Curry' xs@.  This generalises @('.')@ (aka
      -- 'fmap' for @(->)@) to work for curried functions with one argument for each
      -- type in the list.
      composeN :: (i -> j) -> Curry xs i -> Curry xs j

    instance CurryCompose '[] where
      composeN :: forall i j. (i -> j) -> Curry '[] i -> Curry '[] j
    composeN = (i -> j) -> i -> j
    (i -> j) -> Curry '[] i -> Curry '[] j
    forall a. a -> a
    id

    instance CurryCompose xs => CurryCompose (x ': xs) where
      composeN :: forall i j. (i -> j) -> Curry (x : xs) i -> Curry (x : xs) j
    composeN i -> j
    ij Curry (x : xs) i
    f = forall (xs :: IxList) i j.
    CurryCompose xs =>
    (i -> j) -> Curry xs i -> Curry xs j
    composeN @xs i -> j
    ij (Curry xs i -> Curry xs j) -> (x -> Curry xs i) -> x -> Curry xs j
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Curry (x : xs) i
    x -> Curry xs i
    f

    ----------------------------------------
    -- Indices

    -- | Tagged version of 'Data.Type.Equality.(:~:)' for carrying evidence that two
    -- index lists in a curried form are equal.
    data IxEq i is js where
      IxEq :: IxEq i is is

    -- | In pseudo (dependent-)Haskell, provide a witness
    --
    -- @
    -- foldr f (foldr f init xs) ys = foldr f init (ys ++ xs)
    --    where f = (->)
    -- @
    --
    -- @since 0.4
    --
    class AppendIndices xs ys ks | xs ys -> ks where
      appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)

    -- | If the second list is empty, we can pick the first list
    -- even if nothing is known about it.
    instance {-# INCOHERENT #-} xs ~ zs => AppendIndices xs '[] zs where
      appendIndices :: forall i. IxEq i (Curry xs (Curry '[] i)) (Curry zs i)
    appendIndices = IxEq i (Curry xs (Curry '[] i)) (Curry zs i)
    IxEq i (Curry zs i) (Curry zs i)
    forall {k} {k} (i :: k) (is :: k). IxEq i is is
    IxEq

    instance ys ~ zs => AppendIndices '[] ys zs where
      appendIndices :: forall i. IxEq i (Curry '[] (Curry ys i)) (Curry zs i)
    appendIndices = IxEq i (Curry zs i) (Curry zs i)
    IxEq i (Curry '[] (Curry ys i)) (Curry zs i)
    forall {k} {k} (i :: k) (is :: k). IxEq i is is
    IxEq

    instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where
      appendIndices :: forall i. IxEq i (Curry (x ': xs) (Curry ys i)) (Curry (x ': ks) i)
      appendIndices :: forall i. IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i)
    appendIndices | IxEq i (Curry xs (Curry ys i)) (Curry ks i)
    IxEq <- forall (xs :: IxList) (ys :: IxList) (ks :: IxList) i.
    AppendIndices xs ys ks =>
    IxEq i (Curry xs (Curry ys i)) (Curry ks i)
    appendIndices @xs @ys @ks @i = IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i)
    IxEq i (x -> Curry ks i) (x -> Curry ks i)
    forall {k} {k} (i :: k) (is :: k). IxEq i is is
    IxEq

    ----------------------------------------
    -- Either

    -- | If lhs is 'Right', return it. Otherwise check rhs.
    type family FirstRight (m1 :: Either e a) (m2 :: Either e a) :: Either e a where
      FirstRight ('Right a) _ = 'Right a
      FirstRight          _ b = b

    type family FromRight (def :: b) (e :: Either a b) :: b where
      FromRight _   ('Right b) = b
      FromRight def ('Left  _) = def

    type family IsLeft (e :: Either a b) :: Bool where
      IsLeft ('Left _)  = 'True
      IsLeft ('Right _) = 'False

    ----------------------------------------
    -- Errors

    -- | Show a custom type error if @p@ is true.
    type family When (p :: Bool) (err :: Constraint) :: Constraint where
      When 'True  err = err
      When 'False _   = ()

    -- | Show a custom type error if @p@ is false (or stuck).
    type family Unless (p :: Bool) (err :: Constraint) :: Constraint where
      Unless 'True  _   = ()
      Unless 'False err = err

    -- | Use with 'Unless' to detect stuck (undefined) type families.
    type family Defined (f :: k) :: Bool where
      Defined (f _) = Defined f
      Defined _     = 'True

    -- | Show a type surrounded by quote marks.
    type family QuoteType (x :: t) :: ErrorMessage where
      QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’"

    -- | Show a symbol surrounded by quote marks.
    type family QuoteSymbol (x :: Symbol) :: ErrorMessage where
      QuoteSymbol x = 'Text "‘" ':<>: 'Text x ':<>: 'Text "’"

    type family ToOrdinal (n :: Nat) :: ErrorMessage where
      ToOrdinal 1 = 'Text "1st"
      ToOrdinal 2 = 'Text "2nd"
      ToOrdinal 3 = 'Text "3rd"
      ToOrdinal n = 'ShowType n ':<>: 'Text "th"

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

    -- | Derive the shape of @a@ from the shape of @b@.
    class HasShapeOf (a :: k) (b :: k)
    instance {-# OVERLAPPING #-} (fa ~ f a, HasShapeOf f g) => HasShapeOf fa (g b)
    instance (a ~ b) => HasShapeOf a b