{-# 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 Text
Demote Symbol
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