module Internal.Data.Basic.TypeLevel
( AllSatisfy, MappableList(..), Elem, EqualOrError, CheckWithError
, Not, ErrorText, type (++), Without, IsSubset, TypeSatisfies
, OnMaybe, NotNull, ListToTuple
, GHC.ErrorMessage(ShowType, (:<>:), (:$$:))
, GHC.TypeError
) where
import Internal.Interlude
import GHC.TypeLits
import qualified GHC.TypeLits as GHC
type family AllSatisfy (c :: k -> Constraint) (l :: [k]) :: Constraint where
AllSatisfy c '[] = ()
AllSatisfy c (x ': xs) = (c x, AllSatisfy c xs)
class MappableList (l :: [k]) where
mapTypeList :: AllSatisfy c l => proxy1 c -> (forall proxy2 x. c x => proxy2 x -> a) -> proxy3 l -> [a]
instance MappableList '[] where
mapTypeList _ _ _ = []
instance MappableList ks => MappableList (k ': ks) where
mapTypeList pc f _ = f (Proxy :: Proxy k) : mapTypeList pc f (Proxy :: Proxy ks)
type family Elem (x :: k) (xs :: [k]) :: Bool where
Elem x '[] = 'False
Elem x (x ': xs) = 'True
Elem x (y ': xs) = Elem x xs
type family EqualOrError (a :: k) (b :: k) (err :: ErrorMessage) :: Constraint where
EqualOrError a a err = ()
EqualOrError a b err = GHC.TypeError err
type ErrorText = 'GHC.Text
type CheckWithError (b :: Bool) (err :: ErrorMessage) = EqualOrError b 'True err
type family Not (b :: Bool) where
Not 'True = 'False
Not 'False = 'True
type family IsSubset xs ys :: Constraint where
IsSubset '[] ys = ()
IsSubset (x ': xs) ys = (IsTrue (Elem x ys), IsSubset xs ys)
type IsTrue b = b ~ 'True
type family If (condition :: Bool) (t :: k) (e :: k) :: k where
If 'True t e = t
If 'False t e = e
type family Without (xs :: [k]) (ys :: [k]) :: [k] where
Without xs '[] = xs
Without '[] ys = '[]
Without (x ': xs) ys = If (x `Elem` ys) (Without xs ys) (x ': Without xs ys)
type family NotMaybe (a :: *) :: Bool where
NotMaybe (Maybe a) = 'False
NotMaybe a = 'True
type FieldNullErr field =
ErrorText "The field " ':<>: 'ShowType field ':<>: ErrorText " must not be optional (Maybe/Null)"
class CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull (a :: *) (field :: Symbol)
instance CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull a field
type family OnMaybe (a :: k) (f :: b -> k) (m :: Maybe b) :: k where
OnMaybe a f ('Just b) = f b
OnMaybe a f 'Nothing = a
type family FromJust (a :: Maybe x) :: x where
FromJust ('Just x) = x
class c x => TypeSatisfies (c :: * -> Constraint) (x :: *) (field :: Symbol)
instance c x => TypeSatisfies c x field
type family ListToTuple (f :: k -> *) (l :: [k]) where
ListToTuple f '[] = ()
ListToTuple f '[a] = f a
ListToTuple f '[a, b] = (f a, f b)
ListToTuple f '[a, b, c] = (f a, f b, f c)
ListToTuple f '[a, b, c, d] = (f a, f b, f c, f d)
ListToTuple f '[a, b, c, d, e] = (f a, f b, f c, f d, f e)
type family xs ++ ys where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)