{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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 :: forall (a :: PErrorMessage). Sing a -> Demote PErrorMessage
fromSing (SText Sing t
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 [Char]
"Can't single ShowType")
  fromSing (Sing e1
e1 :%<>: Sing e2
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 (Sing e1
e1 :%$$: Sing e2
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 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 (arg :: Symbol). Sing arg -> SErrorMessage ('Text arg)
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 {arg} (arg :: arg).
Sing arg -> SErrorMessage ('ShowType arg)
SShowType ([Char] -> Sing Any
forall a. HasCallStack => [Char] -> a
error [Char]
"Can't single ShowType")
  toSing (ErrorMessage' Text
e1 :<>: ErrorMessage' Text
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
$ \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
$ \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 (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>: Sing a
sE2)
  toSing (ErrorMessage' Text
e1 :$$: ErrorMessage' Text
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
$ \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
$ \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 (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$: Sing a
sE2)

instance SingI t => SingI ('Text t :: PErrorMessage) where
  sing :: Sing ('Text t)
sing = Sing t -> SErrorMessage ('Text t)
forall (arg :: Symbol). Sing arg -> SErrorMessage ('Text arg)
SText Sing t
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI1 ('Text :: Symbol -> PErrorMessage) where
  liftSing :: forall (x :: Symbol). Sing x -> Sing ('Text x)
liftSing = Sing x -> Sing ('Text x)
forall (arg :: Symbol). Sing arg -> SErrorMessage ('Text arg)
SText

instance SingI ty => SingI ('ShowType ty :: PErrorMessage) where
  sing :: Sing ('ShowType ty)
sing = Sing ty -> SErrorMessage ('ShowType ty)
forall {arg} (arg :: arg).
Sing arg -> SErrorMessage ('ShowType arg)
SShowType Sing ty
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI1 ('ShowType :: t -> PErrorMessage) where
  liftSing :: forall (x :: t). Sing x -> Sing ('ShowType x)
liftSing = Sing x -> Sing ('ShowType x)
forall {arg} (arg :: arg).
Sing arg -> SErrorMessage ('ShowType arg)
SShowType

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 (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>: Sing e2
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI e1 => SingI1 ('(:<>:) e1 :: PErrorMessage -> PErrorMessage) where
  liftSing :: forall (x :: PErrorMessage). Sing x -> Sing (e1 ':<>: x)
liftSing Sing x
s = Sing e1
forall {k} (a :: k). SingI a => Sing a
sing Sing e1 -> Sing x -> SErrorMessage (e1 ':<>: x)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>: Sing x
s
instance SingI2 ('(:<>:) :: PErrorMessage -> PErrorMessage -> PErrorMessage) where
  liftSing2 :: forall (x :: PErrorMessage) (y :: PErrorMessage).
Sing x -> Sing y -> Sing (x ':<>: y)
liftSing2 Sing x
s1 Sing y
s2 = Sing x
s1 Sing x -> Sing y -> SErrorMessage (x ':<>: y)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>: Sing y
s2

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 (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$: Sing e2
forall {k} (a :: k). SingI a => Sing a
sing
instance SingI e1 => SingI1 ('(:$$:) e1 :: PErrorMessage -> PErrorMessage) where
  liftSing :: forall (x :: PErrorMessage). Sing x -> Sing (e1 ':$$: x)
liftSing Sing x
s = Sing e1
forall {k} (a :: k). SingI a => Sing a
sing Sing e1 -> Sing x -> SErrorMessage (e1 ':$$: x)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$: Sing x
s
instance SingI2 ('(:$$:) :: PErrorMessage -> PErrorMessage -> PErrorMessage) where
  liftSing2 :: forall (x :: PErrorMessage) (y :: PErrorMessage).
Sing x -> Sing y -> Sing (x ':$$: y)
liftSing2 Sing x
s1 Sing y
s2 = Sing x
s1 Sing x -> Sing y -> SErrorMessage (x ':$$: y)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$: Sing y
s2

-- | 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 Text
t)     = [Char] -> Doc
text (Text -> [Char]
Text.unpack Text
t)
  go (ShowType t
_) = [Char] -> Doc
text [Char]
"<type>" -- Not much we can do here
  go (ErrorMessage' Text
e1 :<>: ErrorMessage' Text
e2) = ErrorMessage' Text -> Doc
go ErrorMessage' Text
e1 Doc -> Doc -> Doc
<> ErrorMessage' Text -> Doc
go ErrorMessage' Text
e2
  go (ErrorMessage' Text
e1 :$$: 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 :: forall a. HasCallStack => 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 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 :: forall {k} (err :: PErrorMessage).
HasCallStack =>
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 {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 TextSym0
forall (arg :: Symbol). Sing arg -> SErrorMessage ('Text arg)
SText

instance SingI (ShowTypeSym0 :: t ~> PErrorMessage) where
  sing :: Sing ShowTypeSym0
sing = SingFunction1 ShowTypeSym0 -> Sing ShowTypeSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 SingFunction1 ShowTypeSym0
forall {arg} (arg :: arg).
Sing arg -> SErrorMessage ('ShowType arg)
SShowType

instance SingI ((:<>:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing :: Sing (:<>:@#@$)
sing = SingFunction2 (:<>:@#@$) -> Sing (:<>:@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 SingFunction2 (:<>:@#@$)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
(:%<>:)
instance SingI x => SingI ((:<>:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing :: Sing ((:<>:@#@$$) x)
sing = SingFunction1 ((:<>:@#@$$) x) -> Sing ((:<>:@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall {k} (a :: k). SingI a => Sing a
forall (a :: PErrorMessage). SingI a => Sing a
sing @x Sing x -> Sing t -> SErrorMessage (x ':<>: t)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>:)
instance SingI1 ((:<>:@#@$$) :: PErrorMessage -> PErrorMessage ~> PErrorMessage) where
  liftSing :: forall (x :: PErrorMessage). Sing x -> Sing ((:<>:@#@$$) x)
liftSing Sing x
s = SingFunction1 ((:<>:@#@$$) x) -> Sing ((:<>:@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s Sing x -> Sing t -> SErrorMessage (x ':<>: t)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':<>: arg)
:%<>:)

instance SingI ((:$$:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
  sing :: Sing (:$$:@#@$)
sing = SingFunction2 (:$$:@#@$) -> Sing (:$$:@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 SingFunction2 (:$$:@#@$)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
(:%$$:)
instance SingI x => SingI ((:$$:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
  sing :: Sing ((:$$:@#@$$) x)
sing = SingFunction1 ((:$$:@#@$$) x) -> Sing ((:$$:@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall {k} (a :: k). SingI a => Sing a
forall (a :: PErrorMessage). SingI a => Sing a
sing @x Sing x -> Sing t -> SErrorMessage (x ':$$: t)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$:)
instance SingI1 ((:$$:@#@$$) :: PErrorMessage -> PErrorMessage ~> PErrorMessage) where
  liftSing :: forall (x :: PErrorMessage). Sing x -> Sing ((:$$:@#@$$) x)
liftSing Sing x
s = SingFunction1 ((:$$:@#@$$) x) -> Sing ((:$$:@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (Sing x
s Sing x -> Sing t -> SErrorMessage (x ':$$: t)
forall (arg :: PErrorMessage) (arg :: PErrorMessage).
Sing arg -> Sing arg -> SErrorMessage (arg ':$$: arg)
:%$$:)

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