{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Base.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.Base.TypeError" at the same time, as many of the
-- definitions in the latter deliberately clash with the former.
--
----------------------------------------------------------------------------
module Data.Singletons.Base.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.Singletons.Internal
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'.
type ErrorMessage' :: Type -> Type
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 :: Type
type ErrorMessage  = ErrorMessage' Text.Text

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

type SErrorMessage :: PErrorMessage -> Type
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 (SText t)      = Text (fromSing t)
  fromSing (SShowType{})  = ShowType (error "Can't single ShowType")
  fromSing (e1 :%<>: e2)  = fromSing e1 :<>: fromSing e2
  fromSing (e1 :%$$: e2)  = fromSing e1 :$$: fromSing e2
  toSing (Text t)     = withSomeSing t  $ SomeSing . SText
  toSing (ShowType{}) = SomeSing $ SShowType (error "Can't single ShowType")
  toSing (e1 :<>: e2) = withSomeSing e1 $ \sE1 ->
                        withSomeSing e2 $ \sE2 ->
                        SomeSing (sE1 :%<>: sE2)
  toSing (e1 :$$: e2) = withSomeSing e1 $ \sE1 ->
                        withSomeSing e2 $ \sE2 ->
                        SomeSing (sE1 :%$$: sE2)

instance SingI t => SingI ('Text t :: PErrorMessage) where
  sing = SText sing
instance SingI1 ('Text :: Symbol -> PErrorMessage) where
  liftSing = SText

instance SingI ty => SingI ('ShowType ty :: PErrorMessage) where
  sing = SShowType sing
instance SingI1 ('ShowType :: t -> PErrorMessage) where
  liftSing = SShowType

instance (SingI e1, SingI e2) => SingI (e1 ':<>: e2 :: PErrorMessage) where
  sing = sing :%<>: sing
instance SingI e1 => SingI1 ('(:<>:) e1 :: PErrorMessage -> PErrorMessage) where
  liftSing s = sing :%<>: s
instance SingI2 ('(:<>:) :: PErrorMessage -> PErrorMessage -> PErrorMessage) where
  liftSing2 s1 s2 = s1 :%<>: s2

instance (SingI e1, SingI e2) => SingI (e1 ':$$: e2 :: PErrorMessage) where
  sing = sing :%$$: sing
instance SingI e1 => SingI1 ('(:$$:) e1 :: PErrorMessage -> PErrorMessage) where
  liftSing s = sing :%$$: s
instance SingI2 ('(:$$:) :: PErrorMessage -> PErrorMessage -> PErrorMessage) where
  liftSing2 s1 s2 = s1 :%$$: s2

-- | Convert an 'ErrorMessage' into a human-readable 'String'.
showErrorMessage :: ErrorMessage -> String
showErrorMessage = show . go
  where
  go :: ErrorMessage -> Doc
  go (Text t)     = text (Text.unpack t)
  go (ShowType _) = text "<type>" -- Not much we can do here
  go (e1 :<>: e2) = go e1 <> go e2
  go (e1 :$$: e2) = go e1 $$ go 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 = error . showErrorMessage

-- | Convert a 'PErrorMessage' to a 'TL.ErrorMessage' from "GHC.TypeLits".
type ConvertPErrorMessage :: PErrorMessage -> TL.ErrorMessage
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 TypeError :: PErrorMessage -> a
type family TypeError (x :: PErrorMessage) :: a where
  -- We cannot define this as a type synonym due to Trac #12048.
  TypeError x = TL.TypeError (ConvertPErrorMessage x)

-- | 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 = typeError . fromSing

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

instance SingI (TextSym0 :: Symbol ~> PErrorMessage) where
  sing = singFun1 SText

instance SingI (ShowTypeSym0 :: t ~> PErrorMessage) where
  sing = singFun1 SShowType

instance SingI ((:<>:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%<>:)
instance SingI x => SingI ((:<>:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%<>:)
instance SingI1 ((:<>:@#@$$) :: PErrorMessage -> PErrorMessage ~> PErrorMessage) where
  liftSing s = singFun1 (s :%<>:)

instance SingI ((:$$:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%$$:)
instance SingI x => SingI ((:$$:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%$$:)
instance SingI1 ((:$$:@#@$$) :: PErrorMessage -> PErrorMessage ~> PErrorMessage) where
  liftSing s = singFun1 (s :%$$:)

instance SingI TypeErrorSym0 where
  sing = singFun1 sTypeError