{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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(SText, SShowType, (:%<>:), (:%$$:)), 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 instance Sing :: PErrorMessage -> Type where
  -- It would be lovely to not have to write those (:: PErrorMessage) kind
  -- ascriptions in the return types of each constructor.
  -- See Trac #14111.
  SText     :: Sing t             -> Sing ('Text t      :: PErrorMessage)
  SShowType :: Sing ty            -> Sing ('ShowType ty :: PErrorMessage)
  (:%<>:)   :: Sing e1 -> Sing e2 -> Sing (e1 ':<>: e2  :: PErrorMessage)
  (:%$$:)   :: Sing e1 -> Sing e2 -> Sing (e1 ':$$: e2  :: PErrorMessage)
infixl 6 :%<>:
infixl 5 :%$$:

type SErrorMessage = (Sing :: PErrorMessage -> Type)

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 SingI ty => SingI ('ShowType ty :: PErrorMessage) where
  sing = SShowType sing

instance (SingI e1, SingI e2) => SingI (e1 ':<>: e2 :: PErrorMessage) where
  sing = sing :%<>: sing

instance (SingI e1, SingI e2) => SingI (e1 ':$$: e2 :: PErrorMessage) where
  sing = sing :%$$: sing

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

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

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

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

instance SingI ((:<>:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%<>:)
instance SingI (TyCon2 '(:<>:) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%<>:)
instance SingI x => SingI ((:<>:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%<>:)
instance SingI x => SingI (TyCon1 ('(:<>:) x) :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%<>:)

instance SingI ((:$$:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%$$:)
instance SingI (TyCon2 '(:$$:) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing = singFun2 (:%$$:)
instance SingI x => SingI ((:$$:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%$$:)
instance SingI x => SingI (TyCon1 ('(:$$:) x) :: PErrorMessage ~> PErrorMessage) where
  sing = singFun1 (sing @x :%$$:)

instance SingI TypeErrorSym0 where
  sing = singFun1 sTypeError