content: {-# LANGUAGE TypeFamilies  #-}
  {-# LANGUAGE TypeInType    #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UnicodeSyntax #-}
  
  {- |
  Copyright:  (c) 2019-2020 Dmitrii Kovanikov
              (c) 2020 Kowainik
  SPDX-License-Identifier: MPL-2.0
  Maintainer: Dmitrii Kovanikov <kovanikov@gmail.com>
              Kowainik <xrom.xkov@gmail.com>
  
  This module provides type-level functions and operators to make the job of
  writing text of custom type errors easier. The motivation behind using custom
  type errors is described in detail in the following blog post:
  
  * [A story told by Type Errors](https://kodimensional.dev/type-errors)
  
  If you want to write the text of a custom error message, you need to use
  constructors of the 'ErrorMessage' data type. But this gets messy and
  inconvenient pretty quickly. Consider the following examples:
  
  @
  __type__ MessageText (e1 :: k) (e2 :: k) (es :: [k]) =
         ''Text' "You require the following two effects from your computation:"
   '':$$:' ''Text' ""
   '':$$:' ''Text' "    '" '':<>:' ''ShowType' e1 '':<>:' ''Text' "' and '" '':<>:' ''ShowType' e2 '':<>:' ''Text' "'"
   '':$$:' ''Text' ""
   '':$$:' ''Text' "However, your monad is capable of performing only the following effects:"
   '':$$:' ''Text' ""
   '':$$:' ''Text' "    " '':<>:' ''ShowType' es
  @
  
  Using combinators from this library, you can define error messages in a simpler
  way:
  
  @
  __type__ MessageText (e1 :: k) (e2 :: k) (es :: [k])
      = "You require the following two effects from your computation:"
      '%' ""
      '%' "    '" 'Type.Errors.Pretty.<>' e1 'Type.Errors.Pretty.<>' "' and '" 'Type.Errors.Pretty.<>' e2 'Type.Errors.Pretty.<>' "'"
      '%' ""
      '%' "However, your monad is capable of performing only the following effects:"
      '%' ""
      '%' "    " 'Type.Errors.Pretty.<>' es
  @
  
  If you prefer, you can use unicode operators to contstruct messages:
  
  @
  __type__ MessageText (e1 :: k) (e2 :: k) (es :: [k])
      = "You require the following two effects from your computation:"
      '•' ""
      '•' "    '" '⊕' e1 '⊕' "' and '" '⊕' e2 '⊕' "'"
      '•' ""
      '•' "However, your monad is capable of performing only the following effects:"
      '•' ""
      '•' "    " '⊕' es
  @
  -}
  
  module Type.Errors.Pretty
         ( -- * Combinators
           type (<>)
         , type (⊕)
         , type (%)
         , type (•)
  
           -- * Reexports from "GHC.TypeLits"
         , TypeError
  
           -- * Helper internal type families
         , ToErrorMessage
         ) where
  
  import GHC.TypeLits (ErrorMessage (..), Symbol, TypeError)
  
  
  {- | Append two types automatically converting them to corresponding
  'ErrorMessage' constructors.
  
  >>> :kind! "Integer values have type: " <> Int
  "Integer values have type: " <> Int :: ErrorMessage
  = 'Text "Integer values have type: " ':<>: 'ShowType Int
  -}
  infixl 5 <>
  type family (<>) (l :: k1) (r :: k2) :: ErrorMessage where
      l <> r = ToErrorMessage l ':<>: ToErrorMessage r
  
  {- | Unicode version of the 'Type.Errors.Pretty.<>' type-level operator.
  -}
  infixl 5 ⊕
  type (⊕) (l :: k1) (r :: k2) = l <> r
  
  {- | Append two types on top of each other automatically converting them to
  corresponding 'ErrorMessage' constructors.
  
  >>> :kind! "Expecting value of type: " % "   " <> Integer
  "Expecting value of type: " % "   " <> Integer :: ErrorMessage
  = 'Text "Expecting value of type: "
    ':$$: ('Text "   " ':<>: 'ShowType Integer)
  -}
  infixr 4 %
  type family (%) (t :: k1) (b :: k2) :: ErrorMessage where
      t % b = ToErrorMessage t ':$$: ToErrorMessage b
  
  {- | Unicode version of the '%' type-level operator.
  -}
  infixr 4 •
  type (•) (t :: k1) (b :: k2) = t % b
  
  -- | Type family to convert any type to 'ErrorMessage'.
  type family ToErrorMessage (t :: k) :: ErrorMessage where
      ToErrorMessage (t :: Symbol) = 'Text t
      ToErrorMessage (t :: ErrorMessage) = t
      ToErrorMessage t = 'ShowType t
  