Internal.Data.Basic.TypeLevel

Documentation

class AllSatisfy c (l :: [k]) where

Minimal complete definition

mapTypeList

Methods

mapTypeList :: proxy1 c -> (forall proxy2 (x :: k). c x => proxy2 x -> a) -> proxy3 l -> [a]

Instances

AllSatisfy k c ([] k)

Methods

mapTypeList :: proxy1 [k] -> (forall (proxy2 :: c -> *) (x :: c). [k] x => proxy2 x -> a) -> proxy3 l -> [a]

(c k, AllSatisfy a c ks) => AllSatisfy a c ((:) a k ks)

Methods

mapTypeList :: proxy1 ((a ': k) ks) -> (forall (proxy2 :: c -> *) (x :: c). (a ': k) ks x => proxy2 x -> a) -> proxy3 l -> [a]

type family Elem (x :: k) (xs :: [k]) :: Bool where ...

Equations

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 ...

Equations

EqualOrError a a err = ()

EqualOrError a b err = TypeError err

type CheckWithError (b :: Bool) (err :: ErrorMessage) = EqualOrError b True err

type family Not (b :: Bool) where ...

Equations

Not True = False

Not False = True

type ErrorText = Text

type family xs ++ ys where ...

Equations

'[] ++ ys = ys

(x ': xs) ++ ys = x ': (xs ++ ys)

type family Without (xs :: [k]) (ys :: [k]) :: [k] where ...

Equations

Without xs '[] = xs

Without '[] ys = '[]

Without (x ': xs) ys = Without' (x `Elem` ys) x xs ys

type family IsSubset xs ys :: Constraint where ...

Equations

IsSubset '[] ys = ()

IsSubset (x ': xs) ys = (IsTrue (Elem x ys), IsSubset xs ys)

class c x => TypeSatisfies (c :: * -> Constraint) (x :: *) (field :: Symbol)

Instances

c x => TypeSatisfies c x field

type family OnMaybe (a :: k) (f :: b -> k) (m :: Maybe b) :: k where ...

Equations

OnMaybe a f (Just b) = f b

OnMaybe a f Nothing = a

class CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull (a :: *) (field :: Symbol)

Instances

CheckWithError (NotMaybe a) (FieldNullErr Symbol field) => NotNull a field

type family ListToTuple (f :: k -> *) (l :: [k]) where ...

Equations

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)

class Trivial a

Instances

Trivial k a

type family SetEqual (as :: [k]) (bs :: [k]) :: Constraint where ...

Equations

SetEqual (a ': as) bs = (IsTrue (Elem a bs), SetEqual as (bs `Without` '[a]))

SetEqual '[] '[] = ()

data ErrorMessage :: * where

A description of a custom type error.

Constructors

ShowType :: ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.

type family TypeError b (a :: ErrorMessage) :: b where ...

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: 4.9.0.0