    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.TypeError
    -- Copyright   :  (C) 2018 Ryan Scott
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines a drop-in replacement for 'TL.TypeError' (from "GHC.TypeLits")
    -- that can be used at the value level as well. Since this is a drop-in
    -- replacement, it is not recommended to import all of "GHC.TypeLits"
    -- and "Data.Singletons.TypeError" at the same time, as many of the definitons
    -- in the latter deliberately clash with the former.
    --
    ----------------------------------------------------------------------------
    module Data.Singletons.TypeError (
      TypeError, sTypeError, typeError,
      ErrorMessage'(..), ErrorMessage, PErrorMessage,
      Sing, SErrorMessage(..),
      ConvertPErrorMessage, showErrorMessage,

      -- * Defunctionalization symbols
      TextSym0, TextSym1,
      ShowTypeSym0, ShowTypeSym1,
      type (:<>:@#@$), type (:<>:@#@$$), type (:<>:@#@$$$),
      type (:$$:@#@$), type (:$$:@#@$$), type (:$$:@#@$$$),
      TypeErrorSym0, TypeErrorSym1
      ) where

    import Data.Kind
    import Data.Singletons.TH
    import qualified Data.Text as Text
    import qualified GHC.TypeLits as TL (ErrorMessage(..), TypeError)
    import GHC.Stack (HasCallStack)
    import GHC.TypeLits hiding (ErrorMessage(..), TypeError)
    import Prelude hiding ((<>))
    import Text.PrettyPrint (Doc, text, (<>), ($$))

    -- | A description of a custom type error.
    --
    -- This is a variation on 'TL.ErrorMessage' that is parameterized over what
    -- text type is used in the 'Text' constructor. Instantiating it with
    -- 'Text.Text' gives you 'ErrorMessage', and instantiating it with 'Symbol'
    -- gives you 'PErrorMessage'.
    data ErrorMessage' s
      = Text s
        -- ^ Show the text as is.
      | forall t. ShowType t
        -- ^ Pretty print the type.
        -- @ShowType :: k -> ErrorMessage@
      | ErrorMessage' s :<>: ErrorMessage' s
        -- ^ Put two pieces of error message next
        -- to each other.
      | ErrorMessage' s :$$: ErrorMessage' s
        -- ^ Stack two pieces of error message on top
        -- of each other.
    infixl 6 :<>:
    infixl 5 :$$:

    -- | A value-level `ErrorMessage'` which uses 'Text.Text' as its text type.
    type ErrorMessage  = ErrorMessage' Text.Text

    -- | A type-level `ErrorMessage'` which uses 'Symbol' as its text kind.
    type PErrorMessage = ErrorMessage' Symbol

    data SErrorMessage :: PErrorMessage -> Type where
      SText     :: Sing t             -> SErrorMessage ('Text t)
      SShowType :: Sing ty            -> SErrorMessage ('ShowType ty)
      (:%<>:)   :: Sing e1 -> Sing e2 -> SErrorMessage (e1 ':<>: e2)
      (:%$$:)   :: Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    infixl 6 :%<>:
    infixl 5 :%$$:

    type instance Sing = SErrorMessage

    instance SingKind PErrorMessage where
      type Demote PErrorMessage = ErrorMessage
      fromSing :: Sing a -> Demote PErrorMessage
    fromSing (SText t)      = Text -> ErrorMessage' Text
    forall s. s -> ErrorMessage' s
    Text (Sing t -> Demote Symbol
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    t)
      fromSing (SShowType{})  = Any -> ErrorMessage' Text
    forall s t. t -> ErrorMessage' s
    ShowType ([Char] -> Any
    forall a. HasCallStack => [Char] -> a
    error "Can't single ShowType")
      fromSing (e1 :%<>: e2)  = Sing e1 -> Demote PErrorMessage
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing e1
    e1 ErrorMessage' Text -> ErrorMessage' Text -> ErrorMessage' Text
    forall s. ErrorMessage' s -> ErrorMessage' s -> ErrorMessage' s
    :<>: Sing e2 -> Demote PErrorMessage
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing e2
    e2
      fromSing (e1 :%$$: e2)  = Sing e1 -> Demote PErrorMessage
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing e1
    e1 ErrorMessage' Text -> ErrorMessage' Text -> ErrorMessage' Text
    forall s. ErrorMessage' s -> ErrorMessage' s -> ErrorMessage' s
    :$$: Sing e2 -> Demote PErrorMessage
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing e2
    e2
      toSing :: Demote PErrorMessage -> SomeSing PErrorMessage
    toSing (Text t)     = Demote Symbol
    -> (forall (a :: Symbol). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote Symbol
    Text
    t  ((forall (a :: Symbol). Sing a -> SomeSing PErrorMessage)
     -> SomeSing PErrorMessage)
    -> (forall (a :: Symbol). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ SErrorMessage ('Text a) -> SomeSing PErrorMessage
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (SErrorMessage ('Text a) -> SomeSing PErrorMessage)
    -> (SSymbol a -> SErrorMessage ('Text a))
    -> SSymbol a
    -> SomeSing PErrorMessage
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SSymbol a -> SErrorMessage ('Text a)
    forall (t :: Symbol). Sing t -> SErrorMessage ('Text t)
    SText
      toSing (ShowType{}) = Sing ('ShowType Any) -> SomeSing PErrorMessage
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing ('ShowType Any) -> SomeSing PErrorMessage)
    -> Sing ('ShowType Any) -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ Sing Any -> SErrorMessage ('ShowType Any)
    forall t (e1 :: t). Sing e1 -> SErrorMessage ('ShowType e1)
    SShowType ([Char] -> Sing Any
    forall a. HasCallStack => [Char] -> a
    error "Can't single ShowType")
      toSing (e1 :<>: e2) = Demote PErrorMessage
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote PErrorMessage
    ErrorMessage' Text
    e1 ((forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
     -> SomeSing PErrorMessage)
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ \sE1 :: Sing a
    sE1 ->
                            Demote PErrorMessage
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote PErrorMessage
    ErrorMessage' Text
    e2 ((forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
     -> SomeSing PErrorMessage)
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ \sE2 :: Sing a
    sE2 ->
                            Sing (a ':<>: a) -> SomeSing PErrorMessage
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    sE1 Sing a -> Sing a -> SErrorMessage (a ':<>: a)
    forall (e1 :: PErrorMessage) (e1 :: PErrorMessage).
    Sing e1 -> Sing e1 -> SErrorMessage (e1 ':<>: e1)
    :%<>: Sing a
    sE2)
      toSing (e1 :$$: e2) = Demote PErrorMessage
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote PErrorMessage
    ErrorMessage' Text
    e1 ((forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
     -> SomeSing PErrorMessage)
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ \sE1 :: Sing a
    sE1 ->
                            Demote PErrorMessage
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote PErrorMessage
    ErrorMessage' Text
    e2 ((forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
     -> SomeSing PErrorMessage)
    -> (forall (a :: PErrorMessage). Sing a -> SomeSing PErrorMessage)
    -> SomeSing PErrorMessage
    forall a b. (a -> b) -> a -> b
    $ \sE2 :: Sing a
    sE2 ->
                            Sing (a ':$$: a) -> SomeSing PErrorMessage
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing a
    sE1 Sing a -> Sing a -> SErrorMessage (a ':$$: a)
    forall (e1 :: PErrorMessage) (e2 :: PErrorMessage).
    Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    :%$$: Sing a
    sE2)

    instance SingI t => SingI ('Text t :: PErrorMessage) where
      sing :: Sing ('Text t)
    sing = Sing t -> SErrorMessage ('Text t)
    forall (t :: Symbol). Sing t -> SErrorMessage ('Text t)
    SText Sing t
    forall k (a :: k). SingI a => Sing a
    sing

    instance SingI ty => SingI ('ShowType ty :: PErrorMessage) where
      sing :: Sing ('ShowType ty)
    sing = Sing ty -> SErrorMessage ('ShowType ty)
    forall t (e1 :: t). Sing e1 -> SErrorMessage ('ShowType e1)
    SShowType Sing ty
    forall k (a :: k). SingI a => Sing a
    sing

    instance (SingI e1, SingI e2) => SingI (e1 ':<>: e2 :: PErrorMessage) where
      sing :: Sing (e1 ':<>: e2)
    sing = Sing e1
    forall k (a :: k). SingI a => Sing a
    sing Sing e1 -> Sing e2 -> SErrorMessage (e1 ':<>: e2)
    forall (e1 :: PErrorMessage) (e1 :: PErrorMessage).
    Sing e1 -> Sing e1 -> SErrorMessage (e1 ':<>: e1)
    :%<>: Sing e2
    forall k (a :: k). SingI a => Sing a
    sing

    instance (SingI e1, SingI e2) => SingI (e1 ':$$: e2 :: PErrorMessage) where
      sing :: Sing (e1 ':$$: e2)
    sing = Sing e1
    forall k (a :: k). SingI a => Sing a
    sing Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    forall (e1 :: PErrorMessage) (e2 :: PErrorMessage).
    Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    :%$$: Sing e2
    forall k (a :: k). SingI a => Sing a
    sing

    -- | Convert an 'ErrorMessage' into a human-readable 'String'.
    showErrorMessage :: ErrorMessage -> String
    showErrorMessage :: ErrorMessage' Text -> [Char]
    showErrorMessage = Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Doc -> [Char])
    -> (ErrorMessage' Text -> Doc) -> ErrorMessage' Text -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ErrorMessage' Text -> Doc
    go
      where
      go :: ErrorMessage -> Doc
      go :: ErrorMessage' Text -> Doc
    go (Text t :: Text
    t)     = [Char] -> Doc
    text (Text -> [Char]
    Text.unpack Text
    t)
      go (ShowType _) = [Char] -> Doc
    text "<type>" -- Not much we can do here
      go (e1 :: ErrorMessage' Text
    e1 :<>: e2 :: ErrorMessage' Text
    e2) = ErrorMessage' Text -> Doc
    go ErrorMessage' Text
    e1 Doc -> Doc -> Doc
    <> ErrorMessage' Text -> Doc
    go ErrorMessage' Text
    e2
      go (e1 :: ErrorMessage' Text
    e1 :$$: e2 :: ErrorMessage' Text
    e2) = ErrorMessage' Text -> Doc
    go ErrorMessage' Text
    e1 Doc -> Doc -> Doc
    $$ ErrorMessage' Text -> Doc
    go ErrorMessage' Text
    e2

    -- | The value-level counterpart to 'TypeError'.
    --
    -- Note that this is not quite as expressive as 'TypeError', as it is unable
    -- to print the contents of 'ShowType' constructors (it will simply print
    -- @\"\<type\>\"@ in their place).
    typeError :: HasCallStack => ErrorMessage -> a
    typeError :: ErrorMessage' Text -> a
    typeError = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a)
    -> (ErrorMessage' Text -> [Char]) -> ErrorMessage' Text -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ErrorMessage' Text -> [Char]
    showErrorMessage

    -- | Convert a 'PErrorMessage' to a 'TL.ErrorMessage' from "GHC.TypeLits".
    type family ConvertPErrorMessage (a :: PErrorMessage) :: TL.ErrorMessage where
      ConvertPErrorMessage ('Text t)      = 'TL.Text t
      ConvertPErrorMessage ('ShowType ty) = 'TL.ShowType ty
      ConvertPErrorMessage (e1 ':<>: e2)  = ConvertPErrorMessage e1 'TL.:<>: ConvertPErrorMessage e2
      ConvertPErrorMessage (e1 ':$$: e2)  = ConvertPErrorMessage e1 'TL.:$$: ConvertPErrorMessage e2

    -- | A drop-in replacement for 'TL.TypeError'. This also exists at the
    -- value-level as 'typeError'.
    type family TypeError (a :: PErrorMessage) :: b where
      -- We cannot define this as a type synonym due to Trac #12048.
      TypeError a = TL.TypeError (ConvertPErrorMessage a)

    -- | The singleton for 'typeError'.
    --
    -- Note that this is not quite as expressive as 'TypeError', as it is unable
    -- to handle 'ShowType' constructors at all.
    sTypeError :: HasCallStack => Sing err -> Sing (TypeError err)
    sTypeError :: Sing err -> Sing (TypeError err)
    sTypeError = ErrorMessage' Text -> Sing (TypeError ...)
    forall a. HasCallStack => ErrorMessage' Text -> a
    typeError (ErrorMessage' Text -> Sing (TypeError ...))
    -> (SErrorMessage err -> ErrorMessage' Text)
    -> SErrorMessage err
    -> Sing (TypeError ...)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SErrorMessage err -> ErrorMessage' Text
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing

    $(genDefunSymbols [''ErrorMessage', ''TypeError])

    instance SingI (TextSym0 :: Symbol ~> PErrorMessage) where
      sing :: Sing TextSym0
    sing = SingFunction1 TextSym0 -> Sing TextSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 TextSym0
    forall (t :: Symbol). Sing t -> SErrorMessage ('Text t)
    SText

    instance SingI (ShowTypeSym0 :: t ~> PErrorMessage) where
      sing :: Sing ShowTypeSym0
    sing = SingFunction1 ShowTypeSym0 -> Sing ShowTypeSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 ShowTypeSym0
    forall t (e1 :: t). Sing e1 -> SErrorMessage ('ShowType e1)
    SShowType

    instance SingI ((:<>:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
      sing :: Sing (:<>:@#@$)
    sing = SingFunction2 (:<>:@#@$) -> Sing (:<>:@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (:<>:@#@$)
    forall (e1 :: PErrorMessage) (e1 :: PErrorMessage).
    Sing e1 -> Sing e1 -> SErrorMessage (e1 ':<>: e1)
    (:%<>:)
    instance SingI x => SingI ((:<>:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
      sing :: Sing ((:<>:@#@$$) x)
    sing = SingFunction1 ((:<>:@#@$$) x) -> Sing ((:<>:@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> SErrorMessage (x ':<>: t)
    forall (e1 :: PErrorMessage) (e1 :: PErrorMessage).
    Sing e1 -> Sing e1 -> SErrorMessage (e1 ':<>: e1)
    :%<>:)

    instance SingI ((:$$:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
      sing :: Sing (:$$:@#@$)
    sing = SingFunction2 (:$$:@#@$) -> Sing (:$$:@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (:$$:@#@$)
    forall (e1 :: PErrorMessage) (e2 :: PErrorMessage).
    Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    (:%$$:)
    instance SingI x => SingI ((:$$:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
      sing :: Sing ((:$$:@#@$$) x)
    sing = SingFunction1 ((:$$:@#@$$) x) -> Sing ((:$$:@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> SErrorMessage (x ':$$: t)
    forall (e1 :: PErrorMessage) (e2 :: PErrorMessage).
    Sing e1 -> Sing e2 -> SErrorMessage (e1 ':$$: e2)
    :%$$:)

    instance SingI TypeErrorSym0 where
      sing :: Sing TypeErrorSym0
    sing = SingFunction1 TypeErrorSym0 -> Sing TypeErrorSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 forall k (err :: PErrorMessage).
    HasCallStack =>
    Sing err -> Sing (TypeError err)
    SingFunction1 TypeErrorSym0
    sTypeError