{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Util.TypeLits
( Symbol
, KnownSymbol
, AppendSymbol
, symbolVal
, symbolValT
, symbolValT'
, TypeError
, ErrorMessage (..)
, TypeErrorUnless
, inTypeErrorUnless
) where
import Data.Constraint (Dict(..))
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
symbolValT :: Proxy s -> Text
symbolValT = String -> Text
forall a. ToText a => a -> Text
toText (String -> Text) -> (Proxy s -> String) -> Proxy s -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal
symbolValT' :: forall s. KnownSymbol s => Text
symbolValT' :: Text
symbolValT' = Proxy s -> Text
forall (s :: Symbol). KnownSymbol s => Proxy s -> Text
symbolValT (Proxy s
forall k (t :: k). Proxy t
Proxy @s)
type family TypeErrorUnless (cond :: Bool) (err :: ErrorMessage) :: Constraint where
TypeErrorUnless 'True _ = ()
TypeErrorUnless 'False err = TypeError err
inTypeErrorUnless
:: forall cond err a.
TypeErrorUnless cond err
=> (cond ~ 'True => a)
-> a
inTypeErrorUnless :: ((cond ~ 'True) => a) -> a
inTypeErrorUnless a :: (cond ~ 'True) => a
a =
case Dict ('True ~ 'True) -> Dict (cond ~ 'True)
forall a b. a -> b
unsafeCoerce @(Dict ('True ~ 'True)) @(Dict (cond ~ 'True)) Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict of
Dict -> a
(cond ~ 'True) => a
a