    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE CPP #-}
    -- | Utilities for working with 'KnownSymbol' constraints.
    module Data.Constraint.Symbol
      ( type AppendSymbol
      , type (++)
      , type Take
      , type Drop
      , type Length
      , appendSymbol
      , appendUnit1
      , appendUnit2
      , appendAssociates
      , takeSymbol
      , dropSymbol
      , takeAppendDrop
      , lengthSymbol
      , takeLength
      , take0
      , takeEmpty
      , dropLength
      , drop0
      , dropEmpty
      , lengthTake
      , lengthDrop
      , dropDrop
      , takeTake
      ) where

    import Data.Constraint
    import Data.Constraint.Nat
    import Data.Constraint.Unsafe
    import Data.Proxy
    import GHC.TypeLits
    #if MIN_VERSION_base(4,18,0)
    import qualified GHC.TypeNats as TN
    #else
    import Unsafe.Coerce
    #endif

    -- | An infix synonym for 'AppendSymbol'.
    type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n
    infixr 5 ++

    type family Take :: Nat -> Symbol -> Symbol where
    type family Drop :: Nat -> Symbol -> Symbol where
    type family Length :: Symbol -> Nat where

    -- implementation details

    #if !MIN_VERSION_base(4,18,0)
    newtype Magic n = Magic (KnownSymbol n => Dict (KnownSymbol n))
    #endif

    magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    #if MIN_VERSION_base(4,18,0)
    magicNSS :: forall (n :: Nat) (m :: Symbol) (o :: Symbol).
    (Int -> String -> String)
    -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    magicNSS Int -> String -> String
    f = ((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
    -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
     -> (KnownNat n, KnownSymbol m) :- KnownSymbol o)
    -> ((KnownNat n, KnownSymbol m) => Dict (KnownSymbol o))
    -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    forall a b. (a -> b) -> a -> b
    $ SSymbol o
    -> (KnownSymbol o => Dict (KnownSymbol o)) -> Dict (KnownSymbol o)
    forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
    withKnownSymbol (forall (s :: Symbol). String -> SSymbol s
    unsafeSSymbol @o (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @n)) Int -> String -> String
    `f` Proxy m -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @m))) Dict (KnownSymbol o)
    KnownSymbol o => Dict (KnownSymbol o)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))
    #endif

    magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
    #if MIN_VERSION_base(4,18,0)
    magicSSS :: forall (n :: Symbol) (m :: Symbol) (o :: Symbol).
    (String -> String -> String)
    -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
    magicSSS String -> String -> String
    f = ((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
    -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub (((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
     -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o)
    -> ((KnownSymbol n, KnownSymbol m) => Dict (KnownSymbol o))
    -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
    forall a b. (a -> b) -> a -> b
    $ SSymbol o
    -> (KnownSymbol o => Dict (KnownSymbol o)) -> Dict (KnownSymbol o)
    forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
    withKnownSymbol (forall (s :: Symbol). String -> SSymbol s
    unsafeSSymbol @o (Proxy n -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @n) String -> String -> String
    `f` Proxy m -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    symbolVal (forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @m))) Dict (KnownSymbol o)
    KnownSymbol o => Dict (KnownSymbol o)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))
    #endif

    magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n
    #if MIN_VERSION_base(4,18,0)
    magicSN :: forall (a :: Symbol) (n :: Nat).
    (String -> Int) -> KnownSymbol a :- KnownNat n
    magicSN String -> Int
    f = (KnownSymbol a => Dict (KnownNat n)) -> KnownSymbol a :- KnownNat n
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((KnownSymbol a => Dict (KnownNat n))
     -> KnownSymbol a :- KnownNat n)
    -> (KnownSymbol a => Dict (KnownNat n))
    -> KnownSymbol a :- KnownNat n
    forall a b. (a -> b) -> a -> b
    $ SNat n -> (KnownNat n => Dict (KnownNat n)) -> Dict (KnownNat n)
    forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
    TN.withKnownNat (forall (n :: Nat). Nat -> SNat n
    unsafeSNat @n (Int -> Nat
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (String -> Int
    f (Proxy a -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    symbolVal (Proxy a
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy a))))) Dict (KnownNat n)
    KnownNat n => Dict (KnownNat n)
    forall (a :: Constraint). a => Dict a
    Dict
    #else
    magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy @a))))
    #endif

    -- operations

    appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
    appendSymbol :: forall (a :: Symbol) (b :: Symbol).
    (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
    appendSymbol = (String -> String -> String)
    -> (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
    forall (n :: Symbol) (m :: Symbol) (o :: Symbol).
    (String -> String -> String)
    -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
    magicSSS String -> String -> String
    forall a. [a] -> [a] -> [a]
    (++)

    appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)
    appendUnit1 :: forall (a :: Symbol). Dict (AppendSymbol "" a ~ a)
    appendUnit1 = Dict (a ~ a)
    Dict (AppendSymbol "" a ~ a)
    forall (a :: Constraint). a => Dict a
    Dict

    appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)
    appendUnit2 :: forall (a :: Symbol). Dict (AppendSymbol a "" ~ a)
    appendUnit2 = Dict (a ~ a)
    Dict (AppendSymbol a "" ~ a)
    forall (a :: Constraint). a => Dict a
    Dict

    appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
    appendAssociates :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol).
    Dict
      (AppendSymbol (AppendSymbol a b) c
       ~ AppendSymbol a (AppendSymbol b c))
    appendAssociates = Dict
      (AppendSymbol (AppendSymbol a b) c
       ~ AppendSymbol a (AppendSymbol b c))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
    takeSymbol :: forall (n :: Nat) (a :: Symbol).
    (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
    takeSymbol = (Int -> String -> String)
    -> (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
    forall (n :: Nat) (m :: Symbol) (o :: Symbol).
    (Int -> String -> String)
    -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    magicNSS Int -> String -> String
    forall a. Int -> [a] -> [a]
    take

    dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
    dropSymbol :: forall (n :: Nat) (a :: Symbol).
    (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
    dropSymbol = (Int -> String -> String)
    -> (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
    forall (n :: Nat) (m :: Symbol) (o :: Symbol).
    (Int -> String -> String)
    -> (KnownNat n, KnownSymbol m) :- KnownSymbol o
    magicNSS Int -> String -> String
    forall a. Int -> [a] -> [a]
    drop

    takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
    takeAppendDrop :: forall (n :: Nat) (a :: Symbol).
    Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
    takeAppendDrop = Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)
    lengthSymbol :: forall (a :: Symbol). KnownSymbol a :- KnownNat (Length a)
    lengthSymbol = (String -> Int) -> KnownSymbol a :- KnownNat (Length a)
    forall (a :: Symbol) (n :: Nat).
    (String -> Int) -> KnownSymbol a :- KnownNat n
    magicSN String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length

    takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)
    takeLength :: forall (n :: Nat) (a :: Symbol). (Length a <= n) :- (Take n a ~ a)
    takeLength = (Assert
       (OrdCond (CmpNat (Length a) n) 'True 'True 'False)
       (TypeError ...) =>
     Dict (Take n a ~ a))
    -> Assert
         (OrdCond (CmpNat (Length a) n) 'True 'True 'False) (TypeError ...)
       :- (Take n a ~ a)
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Take n a ~ a)
    Assert
      (OrdCond (CmpNat (Length a) n) 'True 'True 'False)
      (TypeError ...) =>
    Dict (Take n a ~ a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    take0 :: forall a. Dict (Take 0 a ~ "")
    take0 :: forall (a :: Symbol). Dict (Take 0 a ~ "")
    take0 = Dict (Take 0 a ~ "")
    forall (c :: Constraint). Dict c
    unsafeAxiom

    takeEmpty :: forall n. Dict (Take n "" ~ "")
    takeEmpty :: forall (n :: Nat). Dict (Take n "" ~ "")
    takeEmpty = Dict (Take n "" ~ "")
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")
    dropLength :: forall (n :: Nat) (a :: Symbol). (Length a <= n) :- (Drop n a ~ "")
    dropLength = (Assert
       (OrdCond (CmpNat (Length a) n) 'True 'True 'False)
       (TypeError ...) =>
     Dict (Drop n a ~ ""))
    -> Assert
         (OrdCond (CmpNat (Length a) n) 'True 'True 'False) (TypeError ...)
       :- (Drop n a ~ "")
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub Dict (Drop n a ~ "")
    Assert
      (OrdCond (CmpNat (Length a) n) 'True 'True 'False)
      (TypeError ...) =>
    Dict (Drop n a ~ "")
    forall (c :: Constraint). Dict c
    unsafeAxiom

    drop0 :: forall a. Dict (Drop 0 a ~ a)
    drop0 :: forall (a :: Symbol). Dict (Drop 0 a ~ a)
    drop0 = Dict (Drop 0 a ~ a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dropEmpty :: forall n. Dict (Drop n "" ~ "")
    dropEmpty :: forall (n :: Nat). Dict (Drop n "" ~ "")
    dropEmpty = Dict (Drop n "" ~ "")
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lengthTake :: forall n a. Dict (Length (Take n a) <= n)
    lengthTake :: forall (n :: Nat) (a :: Symbol). Dict (Length (Take n a) <= n)
    lengthTake = Dict
      (Assert
         (OrdCond (CmpNat (Length (Take n a)) n) 'True 'True 'False)
         (TypeError ...))
    Dict
      (Assert
         (OrdCond (Compare (Length (Take n a)) n) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))
    lengthDrop :: forall (n :: Nat) (a :: Symbol).
    Dict (Length a <= (Length (Drop n a) + n))
    lengthDrop = Dict
      (Assert
         (OrdCond
            (CmpNat (Length a) (Length (Drop n a) + n)) 'True 'True 'False)
         (TypeError ...))
    Dict
      (Assert
         (OrdCond
            (Compare (Length a) (Length (Drop n a) + n)) 'True 'True 'False)
         (TypeError ...))
    forall (c :: Constraint). Dict c
    unsafeAxiom

    dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)
    dropDrop :: forall (n :: Nat) (m :: Nat) (a :: Symbol).
    Dict (Drop n (Drop m a) ~ Drop (n + m) a)
    dropDrop = Dict (Drop n (Drop m a) ~ Drop (n + m) a)
    forall (c :: Constraint). Dict c
    unsafeAxiom

    takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)
    takeTake :: forall (n :: Nat) (m :: Nat) (a :: Symbol).
    Dict (Take n (Take m a) ~ Take (Min n m) a)
    takeTake = Dict
      (Take n (Take m a)
       ~ Take (If (OrdCond (CmpNat m n) 'True 'True 'False) m n) a)
    Dict (Take n (Take m a) ~ Take (Min n m) a)
    forall (c :: Constraint). Dict c
    unsafeAxiom